Remember, Haskell is the world's most popular dependently typed functional programming language... (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 _______________________________________________ Agda mailing list Agda@lists.chalmers.se https://lists.chalmers.se/mailman/listinfo/agda