Write a Blog >>
ICFP 2019
Sun 18 - Fri 23 August 2019 Berlin, Germany
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 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
20m
Talk
Syntax with Shifted Names
TyDe
Stephen Dolan , Leo White Jane Street
Pre-print
11:10
20m
Talk
Tic Tac Types (Functional Pearl)
TyDe
Sean Innes University of Bristol, Nicolas Wu Imperial College London
Link to publication
11:30
20m
Talk
Monadic typed tactic programming by reflection
TyDe
Liang-Ting Chen Swansea University
Pre-print
11:50
20m
Talk
Deferring the Details and Deriving Programs
TyDe
Link to publication