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 [4] 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