TyDe 2019 – Proceedings

4th ACM SIGPLAN International Workshop on Type-Driven Development (TyDe 2019)

Frontmatter

Papers

How to do Proofs: Practically Proving Properties about Effectful Programs' Results (Functional Pearl)
Koen Jacobs, Andreas Nuyts, and Dominique Devriese
(KU Leuven, Belgium; Vrije Universiteit Brussel, Belgium)

@InProceedings{TyDe19p1, author = {Koen Jacobs and Andreas Nuyts and Dominique Devriese}, title = {How to do Proofs: Practically Proving Properties about Effectful Programs' Results (Functional Pearl)}, booktitle = {Proc.\ TyDe}, publisher = {ACM}, pages = {1-0}, doi = {10.1145/3331554.3342603}, year = {2019}, } Publisher's Version Article: icfpws19tydemain-p1-p (type: Full Paper) doi:10.1145/3331554.3342603

Generic Level Polymorphic N-ary Functions
Guillaume Allais
(University of Strathclyde, UK)

@InProceedings{TyDe19p14, author = {Guillaume Allais}, title = {Generic Level Polymorphic N-ary Functions}, booktitle = {Proc.\ TyDe}, publisher = {ACM}, pages = {14-13}, doi = {10.1145/3331554.3342604}, year = {2019}, } Publisher's Version Article: icfpws19tydemain-p2-p (type: Full Paper) doi:10.1145/3331554.3342604

Deferring the Details and Deriving Programs
Liam O'Connor
(UNSW, Australia)

@InProceedings{TyDe19p27, author = {Liam O'Connor}, title = {Deferring the Details and Deriving Programs}, booktitle = {Proc.\ TyDe}, publisher = {ACM}, pages = {27-26}, doi = {10.1145/3331554.3342605}, year = {2019}, } Publisher's Version Article: icfpws19tydemain-p4-p (type: Full Paper) doi:10.1145/3331554.3342605

: Video Presentation

Tic Tac Types: A Gentle Introduction to Dependently Typed Programming (Functional Pearl)
Sean Innes and Nicolas Wu
(University of Bristol, UK; Imperial College London, UK)

@InProceedings{TyDe19p40, author = {Sean Innes and Nicolas Wu}, title = {Tic Tac Types: A Gentle Introduction to Dependently Typed Programming (Functional Pearl)}, booktitle = {Proc.\ TyDe}, publisher = {ACM}, pages = {40-39}, doi = {10.1145/3331554.3342606}, year = {2019}, } Publisher's Version Article: icfpws19tydemain-p5-p (type: Full Paper) doi:10.1145/3331554.3342606

: Video Presentation

Inductive Types Deconstructed: The Calculus of United Constructions
Stefan Monnier
(Université de Montréal, Canada)

@InProceedings{TyDe19p53, author = {Stefan Monnier}, title = {Inductive Types Deconstructed: The Calculus of United Constructions}, booktitle = {Proc.\ TyDe}, publisher = {ACM}, pages = {53-52}, doi = {10.1145/3331554.3342607}, year = {2019}, } Publisher's Version Article: icfpws19tydemain-p6-p (type: Full Paper) doi:10.1145/3331554.3342607

Constraint-Based Type-Directed Program Synthesis
Peter-Michael Osera
(Grinnell College, USA)

@InProceedings{TyDe19p66, author = {Peter-Michael Osera}, title = {Constraint-Based Type-Directed Program Synthesis}, booktitle = {Proc.\ TyDe}, publisher = {ACM}, pages = {66-65}, doi = {10.1145/3331554.3342608}, year = {2019}, } Publisher's Version Article: icfpws19tydemain-p10-p (type: Full Paper) doi:10.1145/3331554.3342608

proc time: 0.02