Sun 18 Aug 2019 11:10 - 11:30 at Aurora Borealis - Dependently Typed Programming Chair(s): William J. Bowman
Tic-Tac-Toe is a simple, familiar, classic game enjoyed by many. This pearl is designed to give a flavour of the world of dependent types to the uninitiated functional programmer. We cover a journey from Tic-Tac-Terrible implementations in the harsh world of virtually untyped |Strings|, through the safe haven of vectors that know their own length, and into a Tic-Tac-Titanium version that is too strongly typed for its own good. Along the way we discover something we knew all along; types are great, but in moderation. This lesson is quickly put to use in a more complex recursive version.
Sun 18 AugDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
Sun 18 Aug
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
10:50 - 12:10 | Dependently Typed ProgrammingTyDe at Aurora Borealis Chair(s): William J. Bowman University of British Columbia | ||
10:50 20mTalk | Syntax with Shifted Names TyDe Pre-print | ||
11:10 20mTalk | Tic Tac Types (Functional Pearl) TyDe Link to publication | ||
11:30 20mTalk | Monadic typed tactic programming by reflection TyDe Liang-Ting Chen Swansea University Pre-print | ||
11:50 20mTalk | Deferring the Details and Deriving Programs TyDe Liam O'Connor UNSW Link to publication |