TYPES 2013 Schedule

The schedule for the scientific and other programme of the main conference of TYPES 2013 was as follows, where invited speakers had 60 minutes and the time for contributed talks was 25 minutes, always including discussion and change of speaker.

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

Page maintained by:
Ralph Matthes

Last modified (date in French): dim. mai 12 21:40:38 CEST 2013