The links lead to the PDF files with the slides of the presentations that are provided by their authors for publication on this web site. By the deadline of May 3, 11 a.m. Paris time, slides for the 3 invited talks and 20 contributed talks had been sent. On May 7, six late submissions were put online. On May 12, a further submission (with special permission for this delay) was put online.
Tuesday April 23 09:00 - 09:55 registration - coffee break for arrival 09:55 - 10:00 opening 10:00 - 11:00 inv. talk - session chair: Michael Mendler Awodey. Higher Inductive Types in Homotopy Type Theory 11:00 - 11:30 coffee break 11:30 - 12:45 3 contr. talks - session chair: Sergei Soloviev Herbelin. Some reflections about equality in type theory (tentative material for further research) Ahrens, Kapulkin, Shulman. Univalent categories and the Rezk completion Rijke, Spitters. Sets in homotopy type theory 12:45 - 14:25 100 minutes lunch break 14:25 - 16:05 3 contr. talks - session chair: Tim Sheard Herbelin, Spiwack. The Rooster and the Syntactic Bracket Ahman, Uustalu. Update monads: cointerpreting directed containers Pédrot. A Dependent Delimited Continuation Monad 16:05 - 16:35 coffee break 16:35 - 18:15 4 contr. talks - session chair: Lars Birkedal Chaudhuri, Despeyroux. A Hybrid Linear Logic for Constrained Transition Systems Allamigeon, Gaubert, Magron, Werner. Formal Non-linear Optimization via Templates and Sum-of-Squares Fridlender, Pagano, Rodríguez. Mechanized semantics for an Algol-like language Krebbers. Effective Types for C formalized in Coq Wednesday April 24 09:00 - 10:00 inv. talk - session chair: Stefano Berardi Kohlenbach. Types in Proof Mining 10:00 - 10:25 contr. talk Sato, Pollack, Schwichtenberg, Sakurai. Viewing Lambda-Terms through Maps 10:25 - 10:55 coffee break 10:55 - 13:00 4 contr. talks - session chair: Hugo Herbelin Aschieri, Berardi, Birolo. Strong Normalization for Intuitionistic Arithmetic with 1-Excluded Middle Dapoigny, Barlatier. Formalizing Subsumption Relations in Ontologies using Type Classes in Coq Luo, Part. Subtyping in Type Theory: Coercion Contexts and Local Coercions Retoré. Type-theoretical natural language semantics: on the system F for meaning assembly 13:00 - 14:40 100 minutes lunch break 14:40 - 15:55 3 contr. talks - session chair: Herman Geuvers Abel, Setzer. Copatterns: Programming Infinite Structures by Observations van Bakel, Vigliotti. Fully abstract semantics of lambda-mu with explicit substitution in the pi-calculus Ciaffaglione, Scagnetto. Revisiting the bookkeeping technique in HOAS based encodings 15:55 - 16:25 coffee break 16:25 - 17:40 3 contr. talks - session chair: Randy Pollack Cohen, Dénès, Mörtberg. Computable Refinements by Quotients and Parametricity Claret, González Huesca, Régis-Gianas, Ziliani. Lightweight proof by reflection using a posteriori simulation of effectful computation Werner. A very generic implementation of data-types with binders in Coq 17:40 - 18:00 fresh air break 18:00 - 19:00 business meeting (in French: assemblée générale) - chair: Tarmo Uustalu Thursday April 25 09:00 - 10:00 inv. talk - session chair: Ralph Matthes Birkedal. Charge! a framework for higher-order separation logic in Coq. (information including presentation slides of the preparatory tutorial on Monday) 10:00 - 10:25 contr. talk - session chair: Tarmo Uustalu Ahn, Sheard, Fiore. Mendler-style Recursion Schemes for Mixed-Variant Datatypes 10:25 - 10:55 coffee break 10:55 - 12:35  3 contr. talks - session chair: Benjamin Werner Setzer. Unfolding Nested Patterns and Copatterns [Beauquier. Towards Infinite Terms in Twelf] Sozeau. Universe Polymorphism and Inference in Coq Bezem, Coquand, Nakata. Are streamless sets Noetherian? 12:35 - 14:15 100 minutes lunch break 14:15 - 14:30 gathering for guided visit 14:30 - 16:00 guided visit of old town (if registered) 16:00 - 19:00 free time 19:00 - 20:00 first part of gala dinner: "cocktail" (if registered) 20:00 - 23:00 second part of gala dinner: dinner (if registered - the tickets are compulsory for indicating the chosen menu) Friday April 26 09:30 - 10:45 3 contr. talks - session chair: Zhaohui Luo Maksimović. Probability Logics in Coq Schubert, Urzyczyn, Walukiewicz-Chrząszcz. Positive Logic Is 2-Exptime Hard Blot. Realizability for Peano Arithmetic with Winning Conditions in HON Games 10:45 - 11:15 coffee break 11:15 - 12:30 3 contr. talks - session chair: Steffen van Bakel Berardi. A learning-based interpretation for polymorphic lambda-calculus Ljunglöf. Type-based Human-Computer Interaction Guenot. Nested Typing and Communication in the lambda-calculus 12:30 - 14:10 100 minutes lunch break Those who wanted to attend the workshop CSPM had to leave before 13:45, thus after 75 minutes of lunch (count 10 minutes walk, 20 minutes subway, 10 minutes walk and orientation in the building). 14:30 beginning in IMT
Last modified (date in French): dim. mai 12 21:40:38 CEST 2013