Types 2011 Program

Thursday 8th of September

9:00- Registration

9:25-9:30 Workshop opening by Marc Bezem

Session 1 Curry-Howard
9:30-10:00 Extended Curry-Howard Correspondence: The Case of Loeb Logic  Tadeusz Litak
10:00-10:30 On the Curry-Howard Correspondence for Constructive Modal Logic CK  Michael Mendler
10:30-11:00 Coffee Break

Session 2 Logics
11:00-11:30 Model Theory of Logic-Enriched Type Theories  Robin Adams
11:30-12:00 Extension of General Logic  Patrik Eklund and Robert Helgesson
12:00-12:30 Decision Problems in Intersection Logics  Pawel Urzyczyn
12:30-14:00 Lunch Break

Session 3 Category Theory
14:00-14:30 Algebraic Foundations for Type Theories  Marcelo Fiore
14:30-15:00 Computing in a Boolean Topos  Arnaud Spiwack
15:00-15:30 Abstract Structural Induction  Robert Atkey, Patricia Johann and Neil Ghani
15:30-16:00 Coffee Break

Session 4 Induction
16:00-16:30 A Monoidal Category of Inductive Recursive Definitions  Neil Ghani, Peter Hancock, Conor Mcbride and Lorenzo Malatesta
16:30-17:00 An Equivalence between Small Induction Recursion and Indexed Containers  Lorenzo Malatesta, Thorsten Altenkirch, Neil Ghani, Peter Hancock and Conor Mcbride
17:00-17:30 Elimination Principles for Initial Dialgebras  Fredrik Nordvall Forsberg, Thorsten Altenkirch, Peter Morris and Anton Setzer

Friday 9th of September
Session 5 Invited Talk
9:00-10:00 Type Design Patterns for Computer Proofs  Georges Gonthier, Cambridge
10:00-10:30Coffee Break

Session 6
10:30-11:00 Ornaments: Organising the Zoo of Data-types  Pierre-Evariste Dagand and Conor Mcbride
11:00-11:30 Logical Predicates as First-Class Citizens in LF  Furio Honsell, Marina Lenisa, Luigi Liquori, Petar Maksimovic and Ivan Scagnetto
11:30-12:00 A User-extensible and Safe Alternative to the Conversion Rule using VeriML  Antonis Stampoulis and Zhong Shao
12:00-12:30 Context-dependent Computation using Comodels of Theories in Type Theory  Tarmo Uustalu
12:30-14:00 Lunch Break

Session 7 Formalised Mathematics/Arithmetics/Geometry
14:00-14:30 Certified Polynomial Approximation for Solving the Table Maker's Dilemma  Nicolas Brisebarre, Mioara Joldes, Erik Martin-Dorel, Micaela Mayero, Jean-Michel Muller, Ioana Pasca, Laurence Rideau and Laurent Théry
14:30-15:00 Real Algebraic Geometry: A Formalization of a Quantifier Elimination Procedure for the Theory of Real Closed Field  Cyril Cohen and Assia Mahboubi
15:00-15:30 Formalizing a Discrete Model of the Continuum in Coq from a Discrete Geometry Perspective  Nicolas Magaud, Agathe Chollet and Laurent Fuchs
15:30-16:00 Coffee Break

Session 8 Constructive Mathematics/Algebra
16:00-16:30 Infinite Sets that Satisfy the Principle of Omniscience in all Varieties of Constructive Mathematics  Martin Escardo
16:30-17:00 Type Classes for Efficient Exact Real Arithmetic in Coq  Robbert Krebbers and Bas Spitters
17:00-17:30 Rings with Explicit Divisibility Formalized in Coq  Anders Mörtberg and Cyril Cohen
17:30 TYPES business meeting (agenda: next workshop, post-proceedings, ...)

Saturday 10th of September
Session 9 Invited Talk
9:00-10:00 Sequential versus Continuous Models of Finite Types  Dag Normann, Oslo
10:00-10:30 Coffee Break

Session 10 Typing and Subtyping
10:30-11:00 Comparative Study of Different Styles of Coinductive Logic Programming for Type Inference  Ekaterina Komendantskaya
11:00-11:30 Mechanizing Metatheory without Typing Contexts  Sungwoo Park
11:30-12:00 The Principal Subtyping Theorem and the Subtyping Hierarchy of Lambda Terms  Andrew Polonsky
12:00-12:30 Type-Theoretical Semantics with Coercive Subtyping  Zhaohui Luo
12:30-14:00 Lunch Break

Session 11 Type Systems
14:00-14:30 A Type System for Positivity  Matteo Acerbi, Dominic Mulligan and Claudio Sacerdoti Coen
14:30-15:00 The Role of Second-order Quantification in Soft Type Assignment Systems  Aleksy Schubert, Jacek Chrząszcz and Ken-Etsu Fujita
15:00-15:30 PTS with Typed Equality and Explicit Substitutions  Daniel Fridlender and Miguel Pagano
15:30-15:45 Coffee Break (short)

Session 12 Type Systems/Lambda Calculus
15:45-16:15 On Vectorial Typing  Alejandro Díaz-Caro
16:15-16:45 Exploring the Reach of Hereditary Substitution  Harley D. Eades Iii and Aaron Stump
16:45-17:15 A Characterization of Reduction 1-Cycles in Infinitary Lambda Calculus  Andrew Polonsky and Jörg Endrullis

Workshop Dinner
17:30 Walk to Dreggekaien on Bryggen, boat to Cornelius restaurant leaves 18:00 (sharp)

Sunday 11th of September
Session 13 Invited Talk
9:30-10:30 Resizing rules - their use and semantic justification Vladimir Voevodsky, Princeton
10:30-11:00 Coffee Break

Session 14
11:00-11:30 Formal Proofs of Robustness for Watermarking Algorithms  David Baelde, Pierre Courtieu, David Gross-Amblard, Christine Paulin and Xavier Urbain
11:30-12:00 Prototype Implementation of an Inhabitation Algorithm for FCL$(\cap, \leq)$  Boris Duedder, Moritz Martens and Jakob Rehof
12:00-12:30 Economic Equilibriai in Type Theory  Cezar Ionescu
12:30-14:00 Lunch Break

Session 15
14:00-14:30 Initiality for Typed Syntax and Semantics  Benedikt Ahrens
14:30-15:00 The Link between the Intensional Level and the Extensional one in the Minimalist Foundation  Maria Emilia Maietti
15:00-15:30 Towards a Computational Justification of the Axiom of Univalence  Simon Huber and Thierry Coquand
15:30-16:00 A Computational Proof of Dependent Choice Compatible with Classical Logic  Hugo Herbelin
16:00-16:30 Coffee Break

16:30-22:00 Excursion (hike with meal on Ulriken)

Subpages (1): Talks with abstracts