DTP 2013
ACM SIGPLAN Workshop on Dependently-Typed Programming
DTP 2013 Program
09:00-10:10 - Two Reflections and a Pearl
Welcome and session chair: Stephanie Weirich (University of Pennsylvania)
First-class Type-safe Reflection in Idris Edwin Brady (University of St. Andrews)
Compositional and Customizable Reflective Proofs Gregory Malecha (Harvard SEAS)
Functional Pearl: Four slot asynchronous communication mechanism Matthew Danish (Boston University)
10:10-10:30 - Break
10:30-11:10 - Semantics
Session chair: Brigitte Pientka (McGill University)
Dependent Lambda Encoding with Self Types Peng Fu (University of Iowa)
Deciding intentional equality of total-inductive functions Larry Diehl (Portland State University)
11:10-11:50 - Break
11:50-12:30 - Reasoning and Automation
Session chair: Edwin Brady (University of St. Andrews)
Indexed copatterns: reasoning about infinite structures by
observations David Thibodeau (McGill University)Mining opportunities for unique inhabitants in dependent programs Gabriel Scherer (INRIA Paris-Rocquencourt)
12:30-14:00 - Lunch
14:00-15:00 - Semantics and Design
Session chair: Aaron Stump (University of Iowa)
New Equations for Neutral Terms: A Sound and Complete Decision Procedure, Formalized Guillaume Allais (University of Strathclyde), Pierre Boutillier (Pierre Boutillier) and Conor Mcbride (University of Strathclyde)
A Multivalued Language with a Dependent Type System Neal Glew (Intel Labs), Tim Sweeney (Epic Games) and Leaf Petersen (Intel Labs)
15:00-15:20 - Break
15:20-16:20 - Programming techniques
Session chair: Nils Anders Danielsson (Chalmers and University of Gothenburg)
Relational Algebraic Ornaments Hsiang-Shang Ko and Jeremy Gibbons (Oxford University)
Leveling Up Dependent Types - Generic programming over a predicative hierarchy of universes Larry Diehl and Tim Sheard (Portland State University)
16:20-16:40 - Break
16:40-17:10 - Applications
Session chair: TBA
- Correct-by-Construction Pretty-Printing Nils Anders Danielsson (Chalmers and University of Gothenburg)
17:10 - Closing
- Note, the presentation Refinement Types For Haskell by Ranjit Jhala (UCSD) was cancelled.
Important Dates
Paper Submission:Friday, 14th June 2013, anywhere on Earth
Author Notification:
Thursday, 11th July 2013
Final Papers Due:
Thursday, 25th July 2013
Talk Proposals:
Friday, 16th August 2013
Workshop:
Tuesday, 24th September 2013