Warning: mysql_connect(): Can't connect to MySQL server on 'sosna.mimuw.edu.pl' (113) in /home/misc/types10/public_html/content/registration/classes/DB.class.php on line 14 Warning: mysql_select_db() expects parameter 2 to be resource, boolean given in /home/misc/types10/public_html/content/registration/classes/DB.class.php on line 16 Warning: mysql_query() expects parameter 2 to be resource, boolean given in /home/misc/types10/public_html/content/registration/classes/DB.class.php on line 56 Warning: mysql_error() expects parameter 1 to be resource, boolean given in /home/misc/types10/public_html/content/registration/classes/DB.class.php on line 58 Warning: mysql_query() expects parameter 2 to be resource, boolean given in /home/misc/types10/public_html/content/registration/classes/DB.class.php on line 56 Warning: mysql_error() expects parameter 1 to be resource, boolean given in /home/misc/types10/public_html/content/registration/classes/DB.class.php on line 58 Notice: A session had already been started - ignoring session_start() in /home/misc/types10/public_html/content/registration/classes/Session.class.php on line 16 TYPES 2010 Program

TYPES 2010

PTM UW

All abstracts in PDF file


Wednesday, October 13th

9.00 - 11.00 Registration (coffee from 10:30)

11.00 - 11.10 Opening

11:10 - 12:10 Session 1: Invited talk
Chair: Silvia Ghilezan

Lambda calculus with types [slides]
Henk Barendregt

12:10 - 13:50 Lunch

13:50 - 15:30 Session 2: Proof assistants
Chair: Randy Pollack
(13:50 - 14:15) Treating sets as types in a proof assistant for ordinary mathematics [slides]
Sebastian Reichelt
(14:15 - 14:40) A canonical locally named formalization of an algebraic logical framework
Wilmer Ricciotti
(14:40 - 15:05) Formalization of Hensel's lemma in Coq
Érik Martin-Dorel
(15:05 - 15:30) Fancy examples of proofs in PML
Christophe Raffalli

15:30 - 16:00 Coffee break

16:00 - 17:55 Session 3: Foundations - typed systems
Chair: Luís Pinto
(16:00-16:25) Expansion for universal quantifiers
Sergueï Lenglet
(16:25-16:50) A graphical game semantics for response categories
Florian Hatat
(16:50-17:15) Superdeduction in lambda bar mu mu tilde
Clement Houtmann
(17:15-17:35) Sums in algebraic lambda-calculi
Alejandro Díaz-Caro
(17:35-17:55) A vectorial type system (Work-in-progress)
Alejandro Díaz-Caro

19:00 Reception (Pałac Kazimierzowski, main University campus)



Thursday, October 14th

9:00 - 10:10 Session 4: Invited talk
Chair: Sergei Soloviev

(9:00- 9:50) Machine translation and type theory (invited talk) [slides]
Aarne Ranta
(9:50 - 10:10) Some interesting features of the Polish language in GF
Adam Slaski

10:10 - 10:40 Coffee break

10:40- 12:20 Session 5: From nature to types
Chair: Tarmo Uustalu
(10:40 - 11:05) Proving versus testing in climate impact research
Cezar Ionescu
(11:05 - 11:30) Towards a simply typed CALculus for semantic knowledge bases
Stephan Scheele
(11:30 - 11:55) Small scale reflection, a guided tour [slides]
Assia Mahboubi
(11:55 - 12:20) Formalized foundations of polynomial real analysis [slides]
Cyril Cohen

12:20 - 14:00 Lunch

14:00 - 15:40 Session 6: Highly expressive type systems
Chair: Zhaohui Luo
(14:00 - 14:25) Inductive types in Less Naive Type Theory [slides]
Agnieszka Kozubek
(14:25 - 14:50) Interpreting inductive-inductive definitions as indexed inductive definitions [slides]
Fredrik Nordvall Forsberg
(14:50 - 15:15) Towards a sequent calculus formulation of the calculus of inductive constructions
Jeffrey Sarnat
(15:15 - 15:40) Realizability and parametricty in Pure Type Systems
Marc Lasson

15:40 - 16:10 Coffee break

16:10 - 17:50 Session 7: Foundations - lambda calculus
Chair: Michael Mendler
(16:10 - 16:35) Rewriting modulo associativity and commutativity in Coq.
Thomas Braibant
(16:35 - 17:00) Asymptotically almost all lambda terms are strongly normalizing
Katarzyna Grygiel
(17:00 - 17:25) Reductions between lambda calculus and combinatory logic
Jarosław Tworek
(17:25 - 17:50) Range property for H [slides]
Andrew Polonsky

17:50 - 18:00 Fresh air break

18:00 Business meeting
Chair: Marino Miculan



Friday, October 15th

9:00 - 10:00 Session 8: Invited talk
Chair: Thorsten Altenkirch

Formal verification : from computational geometry to real algebraic geometry
Yves Bertot

10:00 - 10:30 Coffee break

10:30 - 12:10 Session 9: Around proof assistants
Chair: Christophe Raffalli
(10:30 - 10:55) Proof reuse in logical frameworks [slides]
Robin Adams
(10:55 - 11:20) Equations: a dependent pattern-matching compiler
Matthieu Sozeau
(11:20 - 11:45) Proving Coq extraction in Coq
Stéphane Glondu
(11:45 - 12:10) Certified Complexity
Claudio Sacerdoti Coen

12:10 - 13:50 Lunch

13:50 - 15:30 Session 10: Subtyping and coercions
Chair: Marc Bezem
(13:50 - 14:15) Some non-standard reductions in UTT:properties and applications.
Sergei Soloviev
(14:15 - 14:40) Contextual coercive subtyping
Tao Xue
(14:40 - 15:05) A calculus of coercions proving the strong normalization of MLF
Paolo Tranquilli
(15:05 - 15:30) Nonuniform coercions via unification hints
Enrico Tassi

15:30 - 16 Coffee break

16:00 - 17:40 Session 11: Induction and co-induction
Chair: Bengt Nordström
(16:00 - 16:25) Toposes of polynomial coalgebras
Ondrej Rypacek
(16:25 - 16:50) Walking through infinite trees with mixed induction and coinduction [slides]
Keiko Nakata
(16:50 - 17:15) Type-theoretic structured general corecursion [slides]
Tarmo Uustalu
(17:15 - 17:40) Mixed induction/coinduction [slides]
Thorsten Altenkirch

20:00 Conference dinner, "Kuźnia Smaku", Mazowiecka 10.



Saturday, October 16th

9:00 - 10:00 Session 12: Invited talk
Chair: Ugo de'Liguoro

The duality of computation under focus [slides]
Pierre-Louis Curien

10:00 - 10:30 Coffee break

10:30 - 12:10 Session 12 A: Logic
Chair: Marek Zaionc
(10:30 - 10:55) A type system for classical logic with partial functions
Hans de Nivelle
(10:55 - 11:20) Resource control in sequent lambda calculus [slides]
Silvia Ghilezan
(11:20 - 11:45) Monadic translation of classical sequent calculus with application to strong normalisation
Luís Pinto
(11:45 - 12:10) A computational analysis of Gödel's completeness theorem [slides]
Hugo Herbelin

12:10 - 13:50 Lunch


Information for speakers

We expect that presentations will be prepared as PDF files. It is enough if you bring yours on a USB memory stick and/or send it to us by e-mail (no later than on Monday, October 11). You do not need to use your own computer, there will be one dedicated for presentations. The beamer to be used is OPTOMA EP 759. Currently we do NOT plan using an overhead projector. There will be a flipchart too, but no blackboard.

In case your needs are exceeding the above (for instance you want to use PowerPoint) please notify us ahead of time. If you must use your own computer, make sure before the session that the connection with beamer works properly. If it is a Mac, remember to bring the necessary adapter.

We do not have any time left for demos. Since coffee breaks are going to be served in the same room, informal demo sessions can be arranged during breaks.

Abstracts