[Agda] DTP 2010: call for participation
Thorsten Altenkirch
txa at Cs.Nott.AC.UK
Thu May 6 14:28:56 CEST 2010
(s:S)*(p:P s)->(s:S)*(p:P s)->(s:S)*(p:P s)->(s:S)*(p:P s)->(s:S)*(p:P s)->
DTP 2010 --- Call for Participation
EARLY REGISTRATION ENDS 17 MAY 2010
Workshop on DEPENDENTLY TYPED PROGRAMMING
Edinburgh, Scotland, 9&10 July 2010
(a FLoC workshop, affiliated with LICS)
http://sneezy.cs.nott.ac.uk/darcs/dtp10/
(s:S)*(p:P s)->(s:S)*(p:P s)->(s:S)*(p:P s)->(s:S)*(p:P s)->(s:S)*(p:P s)->
Roll up! Roll up! Register early, register often!
http://www.floc-conference.org/registration.html
Attendance at DTP10 can be yours at a BARGAIN price if you register BEFORE
17 MAY 2010. The preliminary programme for DTP10 is here:
http://sneezy.cs.nott.ac.uk/darcs/dtp10/programme.html
Invited Talks:
Ana Bove, Chalmers University, "10 Years of Partiality and General Recursion"
Matthieu Sozeau, Harvard University, "Elaborations in Type Theory"
Contributed Talks:
Edwin Brady, "Practical, efficient programming with dependent types"
James Caldwell, "Extracting Monadic Programs form Proofs", (joint work with Josef Pohl)
Adam Chlipala, "Generating Pieces of Web Applications with Type-Level Programming"
Nils Anders Danielsson, TBA
Larry Diehl, "Unit & integration test composition via lemmas"
Makoto Hamana, "Another Initial Algebra Semantics of Inductive Families for Programming"
Hugo Herbelin, "A sequent calculus presentation of the Calculus of Inductive Constructions" (joint work with Jeffrey Sarnat, Vincent Siles)
Karim Kariso, "Integrating Agda and Automated Theorem Proving Techniques" (joint work with Anton Setzer)
Dan Licata, "Security-Typed Programming within Dependently Typed Programming" (joint work with Jamie Morgenstern)
Ulf Norell, TBA
Carsten Schuermann, "The HOL-Nuprl connection in Delphin", (joint work with Adam Poswolsky)
Anton Setzer, "Coalgebras in dependent type theory"
Antonis Stampoulis, "VeriML: Type-safe computation of logical terms inside a language with effects"
Tarmo Uustalu, TBA
Sean Wilson, "Supporting Dependently Typed Functional Programming with Proof Automation and Testing"
If, by some chance, you are interested in talking at DTP10, please do get
in touch. Space in the programme is now very tight, but we remain open to
proposals.
See you in Edinburgh in July!
Thorsten and Conor
More information about the Agda
mailing list