Types logo, by Florent Kirchner

Program of the Workshop

Invited Talks

Richard Garner: Topological and higher-dimensional aspects of type theory

It was observed by Hofmann and Streicher in the 1990s that, in Martin-Löf's intensional type theory, it is possible to endow each type A with a groupoid structure, by taking as the ``type of morphisms'' from a to b, the identity type IdA(a,b). However, it was made clear even at this time that this was not the end of the story. Indeed, the associativity and unitality axioms for this type-theoretic groupoid do not hold on-the-nose, but only up to propositional equality. Thus, if we are to obtain a genuine groupoid from a type, we must first quotient out by propositional equality. A similar phenomenon occurs in the construction of the fundamental group of a topological space: in order that the group operation should be associative on-the-nose, one must quotient out paths by the homotopy relation. This suggests the following analogy: that types are like topological spaces, and that propositional equality is like the homotopy relation. Remarkably, it turns out that this analogy can be made into something precise. The purpose of this talk is to give an overview of the growing body of work which exploits this connection, and to describe some of the challenges that remain.

Pawel Urzyczyn : Decision problems in polymorphic type assignment

This talk will survey known results (some old ones and some new ones) and open questions concerning decision problems related to various type-assignment systems. These decision problems fall into essentially two categories:

  • Typability and type-checking: Given a term M, determine if M can be assigned a given type (or any type at all) in a given (or arbitrary) type environment.
  • Type inhabitation (provability): Given a type t, determine if there is a term M such that M has type t (or equivalently, if t has a proof) in a given type environment.

For the simply typed lambda-calculus, these problems are decidable in polynomial time (type inference) or space (inhabitation). In polymorphic calculi each of them can be undecidable; in particular the famous theorem of Wells states that typability in system F is undecidable. Little is known about decidable subsystems (or variants) of F, for example it is an open problem if typability is decidable in the parametric fragment. In addition to the universal polymorphism of system F and its relatives, this survey will cover the decision problems originating from Curry-style, Church-style and domain-free calculi involving other forms of polymorphism: existential, ad hoc (intersection types) and first-order (dependent types).

Peter Hancock : Entering bars infinitely often

Infinite streams have a natural topology. I'll present a complete representation of continuous functions on streams by data-structures that behave like programs for reading streams and writing values or streams of values. To ensure continuity requires both coinductive and inductive definitions, that on the inductive side, go back to Brouwer's bar-induction. I'll sketch the extension of these ideas to kinds of infinite object more general than streams, where the use of dependent types seems essential.

Joint work with Neil Ghani (Strathclyde) and Dirk Pattinson (Imperial).

Schedule — Notice: Undefined index: abstract_id in /afs/lama.univ-savoie.fr/user/httpd/html/sitelama/Membres/pages_web/types09/program.php on line 75 show all abstracts

May the 11th
19:00 — Cold dinner
May the 12th
09:00 — Registration
12:30 — Lunch
14:00 — Bruno Barras Notice: Undefined index: abstract_id in /afs/lama.univ-savoie.fr/user/httpd/html/sitelama/Membres/pages_web/types09/program.php on line 123 Notice: Undefined index: abstract_id in /afs/lama.univ-savoie.fr/user/httpd/html/sitelama/Membres/pages_web/types09/program.php on line 123 — abstractslides
Extending the Implicit Calculus of Constructions with Union and Subset Types Notice: Undefined index: abstract_id in /afs/lama.univ-savoie.fr/user/httpd/html/sitelama/Membres/pages_web/types09/program.php on line 136 Notice: Undefined index: abstract_id in /afs/lama.univ-savoie.fr/user/httpd/html/sitelama/Membres/pages_web/types09/program.php on line 136
14:30 — Chantal Keller Notice: Undefined index: abstract_id in /afs/lama.univ-savoie.fr/user/httpd/html/sitelama/Membres/pages_web/types09/program.php on line 123 Notice: Undefined index: abstract_id in /afs/lama.univ-savoie.fr/user/httpd/html/sitelama/Membres/pages_web/types09/program.php on line 123 — abstractslides
Importing HOL-Light into Coq : deep and shallow embeddings of the higher order logic into Coq Notice: Undefined index: abstract_id in /afs/lama.univ-savoie.fr/user/httpd/html/sitelama/Membres/pages_web/types09/program.php on line 136 Notice: Undefined index: abstract_id in /afs/lama.univ-savoie.fr/user/httpd/html/sitelama/Membres/pages_web/types09/program.php on line 136
15:00 — Lionel Vaux Notice: Undefined index: abstract_id in /afs/lama.univ-savoie.fr/user/httpd/html/sitelama/Membres/pages_web/types09/program.php on line 123 Notice: Undefined index: abstract_id in /afs/lama.univ-savoie.fr/user/httpd/html/sitelama/Membres/pages_web/types09/program.php on line 123 — abstractslides
Primitive recursion in finiteness spaces Notice: Undefined index: abstract_id in /afs/lama.univ-savoie.fr/user/httpd/html/sitelama/Membres/pages_web/types09/program.php on line 136 Notice: Undefined index: abstract_id in /afs/lama.univ-savoie.fr/user/httpd/html/sitelama/Membres/pages_web/types09/program.php on line 136
15:30 — Coffee Break
16:00 — Cody Roux Notice: Undefined index: abstract_id in /afs/lama.univ-savoie.fr/user/httpd/html/sitelama/Membres/pages_web/types09/program.php on line 123 Notice: Undefined index: abstract_id in /afs/lama.univ-savoie.fr/user/httpd/html/sitelama/Membres/pages_web/types09/program.php on line 123 — abstractslides
Normalisation by set theoretic models and labelling Notice: Undefined index: abstract_id in /afs/lama.univ-savoie.fr/user/httpd/html/sitelama/Membres/pages_web/types09/program.php on line 136 Notice: Undefined index: abstract_id in /afs/lama.univ-savoie.fr/user/httpd/html/sitelama/Membres/pages_web/types09/program.php on line 136
16:30 — Neil Sculthorpe Notice: Undefined index: abstract_id in /afs/lama.univ-savoie.fr/user/httpd/html/sitelama/Membres/pages_web/types09/program.php on line 123 Notice: Undefined index: abstract_id in /afs/lama.univ-savoie.fr/user/httpd/html/sitelama/Membres/pages_web/types09/program.php on line 123 — abstractslides
Safe Functional Reactive Programming through Dependent Types Notice: Undefined index: abstract_id in /afs/lama.univ-savoie.fr/user/httpd/html/sitelama/Membres/pages_web/types09/program.php on line 136 Notice: Undefined index: abstract_id in /afs/lama.univ-savoie.fr/user/httpd/html/sitelama/Membres/pages_web/types09/program.php on line 136
17:00 — Denis Cousineau Notice: Undefined index: abstract_id in /afs/lama.univ-savoie.fr/user/httpd/html/sitelama/Membres/pages_web/types09/program.php on line 123 Notice: Undefined index: abstract_id in /afs/lama.univ-savoie.fr/user/httpd/html/sitelama/Membres/pages_web/types09/program.php on line 123 — abstractslides
How to prove strong normalization from weak normalization, the case of minimal deduction modulo Notice: Undefined index: abstract_id in /afs/lama.univ-savoie.fr/user/httpd/html/sitelama/Membres/pages_web/types09/program.php on line 136 Notice: Undefined index: abstract_id in /afs/lama.univ-savoie.fr/user/httpd/html/sitelama/Membres/pages_web/types09/program.php on line 136
17:45 — Demo session
19:00 — Dinner
May the 13th
09:00 — Pawel Urzyczyn (invited) Notice: Undefined index: abstract_id in /afs/lama.univ-savoie.fr/user/httpd/html/sitelama/Membres/pages_web/types09/program.php on line 123 Notice: Undefined index: abstract_id in /afs/lama.univ-savoie.fr/user/httpd/html/sitelama/Membres/pages_web/types09/program.php on line 123 — abstractslides
Decision problems in polymorphic type assignment Notice: Undefined index: abstract_id in /afs/lama.univ-savoie.fr/user/httpd/html/sitelama/Membres/pages_web/types09/program.php on line 136 Notice: Undefined index: abstract_id in /afs/lama.univ-savoie.fr/user/httpd/html/sitelama/Membres/pages_web/types09/program.php on line 136
10:00 — Johannes Kanig Notice: Undefined index: abstract_id in /afs/lama.univ-savoie.fr/user/httpd/html/sitelama/Membres/pages_web/types09/program.php on line 123 Notice: Undefined index: abstract_id in /afs/lama.univ-savoie.fr/user/httpd/html/sitelama/Membres/pages_web/types09/program.php on line 123 — abstractslides
Proof of Higher-Order Programs using Effect Polymorphism Notice: Undefined index: abstract_id in /afs/lama.univ-savoie.fr/user/httpd/html/sitelama/Membres/pages_web/types09/program.php on line 136 Notice: Undefined index: abstract_id in /afs/lama.univ-savoie.fr/user/httpd/html/sitelama/Membres/pages_web/types09/program.php on line 136
10:30 — Coffee Break
11:00 — Jean Duprat Notice: Undefined index: abstract_id in /afs/lama.univ-savoie.fr/user/httpd/html/sitelama/Membres/pages_web/types09/program.php on line 123 Notice: Undefined index: abstract_id in /afs/lama.univ-savoie.fr/user/httpd/html/sitelama/Membres/pages_web/types09/program.php on line 123 — abstractslides
Plane geometry for pupils in Coq Notice: Undefined index: abstract_id in /afs/lama.univ-savoie.fr/user/httpd/html/sitelama/Membres/pages_web/types09/program.php on line 136 Notice: Undefined index: abstract_id in /afs/lama.univ-savoie.fr/user/httpd/html/sitelama/Membres/pages_web/types09/program.php on line 136
11:30 — Enrico Tassi Notice: Undefined index: abstract_id in /afs/lama.univ-savoie.fr/user/httpd/html/sitelama/Membres/pages_web/types09/program.php on line 123 Notice: Undefined index: abstract_id in /afs/lama.univ-savoie.fr/user/httpd/html/sitelama/Membres/pages_web/types09/program.php on line 123 — abstractslides
Hints in unification Notice: Undefined index: abstract_id in /afs/lama.univ-savoie.fr/user/httpd/html/sitelama/Membres/pages_web/types09/program.php on line 136 Notice: Undefined index: abstract_id in /afs/lama.univ-savoie.fr/user/httpd/html/sitelama/Membres/pages_web/types09/program.php on line 136
12:00 — Claudio Sacerdoti Coen Notice: Undefined index: abstract_id in /afs/lama.univ-savoie.fr/user/httpd/html/sitelama/Membres/pages_web/types09/program.php on line 123 Notice: Undefined index: abstract_id in /afs/lama.univ-savoie.fr/user/httpd/html/sitelama/Membres/pages_web/types09/program.php on line 123 — abstractslides
Matita NG: reduction and type-checking Notice: Undefined index: abstract_id in /afs/lama.univ-savoie.fr/user/httpd/html/sitelama/Membres/pages_web/types09/program.php on line 136 Notice: Undefined index: abstract_id in /afs/lama.univ-savoie.fr/user/httpd/html/sitelama/Membres/pages_web/types09/program.php on line 136
12:30 — Lunch
14:00 — Andreas Abel Notice: Undefined index: abstract_id in /afs/lama.univ-savoie.fr/user/httpd/html/sitelama/Membres/pages_web/types09/program.php on line 123 Notice: Undefined index: abstract_id in /afs/lama.univ-savoie.fr/user/httpd/html/sitelama/Membres/pages_web/types09/program.php on line 123 — abstractslides
Normalization by Evaluation for Impredicative Type Theory (Work in Progress) Notice: Undefined index: abstract_id in /afs/lama.univ-savoie.fr/user/httpd/html/sitelama/Membres/pages_web/types09/program.php on line 136 Notice: Undefined index: abstract_id in /afs/lama.univ-savoie.fr/user/httpd/html/sitelama/Membres/pages_web/types09/program.php on line 136
14:30 — Paola Toto Notice: Undefined index: abstract_id in /afs/lama.univ-savoie.fr/user/httpd/html/sitelama/Membres/pages_web/types09/program.php on line 123 Notice: Undefined index: abstract_id in /afs/lama.univ-savoie.fr/user/httpd/html/sitelama/Membres/pages_web/types09/program.php on line 123 — abstractslides
Algebraic setting for many-valued constructive topology Notice: Undefined index: abstract_id in /afs/lama.univ-savoie.fr/user/httpd/html/sitelama/Membres/pages_web/types09/program.php on line 136 Notice: Undefined index: abstract_id in /afs/lama.univ-savoie.fr/user/httpd/html/sitelama/Membres/pages_web/types09/program.php on line 136
15:00 — Ugo de Liguoro Notice: Undefined index: abstract_id in /afs/lama.univ-savoie.fr/user/httpd/html/sitelama/Membres/pages_web/types09/program.php on line 123 Notice: Undefined index: abstract_id in /afs/lama.univ-savoie.fr/user/httpd/html/sitelama/Membres/pages_web/types09/program.php on line 123 — abstractslides
An interactive concept of integer and boolean to model classical arithmetic constructively Notice: Undefined index: abstract_id in /afs/lama.univ-savoie.fr/user/httpd/html/sitelama/Membres/pages_web/types09/program.php on line 136 Notice: Undefined index: abstract_id in /afs/lama.univ-savoie.fr/user/httpd/html/sitelama/Membres/pages_web/types09/program.php on line 136
15:30 — Coffee Break
16:00 — Randy Pollack Notice: Undefined index: abstract_id in /afs/lama.univ-savoie.fr/user/httpd/html/sitelama/Membres/pages_web/types09/program.php on line 123 Notice: Undefined index: abstract_id in /afs/lama.univ-savoie.fr/user/httpd/html/sitelama/Membres/pages_web/types09/program.php on line 123 — abstractslides
A new canonical representation of binding Notice: Undefined index: abstract_id in /afs/lama.univ-savoie.fr/user/httpd/html/sitelama/Membres/pages_web/types09/program.php on line 136 Notice: Undefined index: abstract_id in /afs/lama.univ-savoie.fr/user/httpd/html/sitelama/Membres/pages_web/types09/program.php on line 136
16:30 — Tom Hirschowitz Notice: Undefined index: abstract_id in /afs/lama.univ-savoie.fr/user/httpd/html/sitelama/Membres/pages_web/types09/program.php on line 123 Notice: Undefined index: abstract_id in /afs/lama.univ-savoie.fr/user/httpd/html/sitelama/Membres/pages_web/types09/program.php on line 123 — abstractslides
Contraction-free proofs and games for Linear Logic Notice: Undefined index: abstract_id in /afs/lama.univ-savoie.fr/user/httpd/html/sitelama/Membres/pages_web/types09/program.php on line 136 Notice: Undefined index: abstract_id in /afs/lama.univ-savoie.fr/user/httpd/html/sitelama/Membres/pages_web/types09/program.php on line 136
17:00 — Matthieu Sozeau Notice: Undefined index: abstract_id in /afs/lama.univ-savoie.fr/user/httpd/html/sitelama/Membres/pages_web/types09/program.php on line 123 Notice: Undefined index: abstract_id in /afs/lama.univ-savoie.fr/user/httpd/html/sitelama/Membres/pages_web/types09/program.php on line 123 — abstractslides
A New Look at Generalized Rewriting in Type Theory Notice: Undefined index: abstract_id in /afs/lama.univ-savoie.fr/user/httpd/html/sitelama/Membres/pages_web/types09/program.php on line 136 Notice: Undefined index: abstract_id in /afs/lama.univ-savoie.fr/user/httpd/html/sitelama/Membres/pages_web/types09/program.php on line 136
17:45 — Demo session
19:00 — Dinner
May the 14th
09:00 — Peter Hancock (invited) Notice: Undefined index: abstract_id in /afs/lama.univ-savoie.fr/user/httpd/html/sitelama/Membres/pages_web/types09/program.php on line 123 Notice: Undefined index: abstract_id in /afs/lama.univ-savoie.fr/user/httpd/html/sitelama/Membres/pages_web/types09/program.php on line 123 — abstractslides
Entering bars infinitely often Notice: Undefined index: abstract_id in /afs/lama.univ-savoie.fr/user/httpd/html/sitelama/Membres/pages_web/types09/program.php on line 136 Notice: Undefined index: abstract_id in /afs/lama.univ-savoie.fr/user/httpd/html/sitelama/Membres/pages_web/types09/program.php on line 136
10:00 — Ioana Pasca Notice: Undefined index: abstract_id in /afs/lama.univ-savoie.fr/user/httpd/html/sitelama/Membres/pages_web/types09/program.php on line 123 Notice: Undefined index: abstract_id in /afs/lama.univ-savoie.fr/user/httpd/html/sitelama/Membres/pages_web/types09/program.php on line 123 — abstractslides
Formal verification of exact computations using Newton\'s method Notice: Undefined index: abstract_id in /afs/lama.univ-savoie.fr/user/httpd/html/sitelama/Membres/pages_web/types09/program.php on line 136 Notice: Undefined index: abstract_id in /afs/lama.univ-savoie.fr/user/httpd/html/sitelama/Membres/pages_web/types09/program.php on line 136
10:30 — Coffee Break
11:00 — Thorsten Altenkirch Notice: Undefined index: abstract_id in /afs/lama.univ-savoie.fr/user/httpd/html/sitelama/Membres/pages_web/types09/program.php on line 123 Notice: Undefined index: abstract_id in /afs/lama.univ-savoie.fr/user/httpd/html/sitelama/Membres/pages_web/types09/program.php on line 123 — abstractslides
PiSigma a core language for dependently typed programming Notice: Undefined index: abstract_id in /afs/lama.univ-savoie.fr/user/httpd/html/sitelama/Membres/pages_web/types09/program.php on line 136 Notice: Undefined index: abstract_id in /afs/lama.univ-savoie.fr/user/httpd/html/sitelama/Membres/pages_web/types09/program.php on line 136
11:30 — Hugo Herbelin Notice: Undefined index: abstract_id in /afs/lama.univ-savoie.fr/user/httpd/html/sitelama/Membres/pages_web/types09/program.php on line 123 Notice: Undefined index: abstract_id in /afs/lama.univ-savoie.fr/user/httpd/html/sitelama/Membres/pages_web/types09/program.php on line 123 — abstractslides
Investigations into Kripke models for classical logic Notice: Undefined index: abstract_id in /afs/lama.univ-savoie.fr/user/httpd/html/sitelama/Membres/pages_web/types09/program.php on line 136 Notice: Undefined index: abstract_id in /afs/lama.univ-savoie.fr/user/httpd/html/sitelama/Membres/pages_web/types09/program.php on line 136
12:00 — Michael Lienhardt Notice: Undefined index: abstract_id in /afs/lama.univ-savoie.fr/user/httpd/html/sitelama/Membres/pages_web/types09/program.php on line 123 Notice: Undefined index: abstract_id in /afs/lama.univ-savoie.fr/user/httpd/html/sitelama/Membres/pages_web/types09/program.php on line 123 — abstractslides
Typing Component-Based Communication Systems Notice: Undefined index: abstract_id in /afs/lama.univ-savoie.fr/user/httpd/html/sitelama/Membres/pages_web/types09/program.php on line 136 Notice: Undefined index: abstract_id in /afs/lama.univ-savoie.fr/user/httpd/html/sitelama/Membres/pages_web/types09/program.php on line 136
12:30 — Lunch
14:00 — Easy mountain walk
17:00 — Business meeting
19:00 — Dinner
May the 15th
09:00 — Richard Garner (invited) Notice: Undefined index: abstract_id in /afs/lama.univ-savoie.fr/user/httpd/html/sitelama/Membres/pages_web/types09/program.php on line 123 Notice: Undefined index: abstract_id in /afs/lama.univ-savoie.fr/user/httpd/html/sitelama/Membres/pages_web/types09/program.php on line 123 — abstractslides
Topological and higher-dimensional aspects of type theory Notice: Undefined index: abstract_id in /afs/lama.univ-savoie.fr/user/httpd/html/sitelama/Membres/pages_web/types09/program.php on line 136 Notice: Undefined index: abstract_id in /afs/lama.univ-savoie.fr/user/httpd/html/sitelama/Membres/pages_web/types09/program.php on line 136
10:00 — Zhaohui Luo Notice: Undefined index: abstract_id in /afs/lama.univ-savoie.fr/user/httpd/html/sitelama/Membres/pages_web/types09/program.php on line 123 Notice: Undefined index: abstract_id in /afs/lama.univ-savoie.fr/user/httpd/html/sitelama/Membres/pages_web/types09/program.php on line 123 — abstractslides
Dependent Record Types Revisited Notice: Undefined index: abstract_id in /afs/lama.univ-savoie.fr/user/httpd/html/sitelama/Membres/pages_web/types09/program.php on line 136 Notice: Undefined index: abstract_id in /afs/lama.univ-savoie.fr/user/httpd/html/sitelama/Membres/pages_web/types09/program.php on line 136
10:30 — Coffee Break
11:00 — Nils Anders Danielsson Notice: Undefined index: abstract_id in /afs/lama.univ-savoie.fr/user/httpd/html/sitelama/Membres/pages_web/types09/program.php on line 123 Notice: Undefined index: abstract_id in /afs/lama.univ-savoie.fr/user/httpd/html/sitelama/Membres/pages_web/types09/program.php on line 123 — abstractslides
Mixing Induction and Coinduction Notice: Undefined index: abstract_id in /afs/lama.univ-savoie.fr/user/httpd/html/sitelama/Membres/pages_web/types09/program.php on line 136 Notice: Undefined index: abstract_id in /afs/lama.univ-savoie.fr/user/httpd/html/sitelama/Membres/pages_web/types09/program.php on line 136
11:30 — Clement Houtmann Notice: Undefined index: abstract_id in /afs/lama.univ-savoie.fr/user/httpd/html/sitelama/Membres/pages_web/types09/program.php on line 123 Notice: Undefined index: abstract_id in /afs/lama.univ-savoie.fr/user/httpd/html/sitelama/Membres/pages_web/types09/program.php on line 123 — abstractslides
Cut-elimination Canonicity for Classical Sequent Calculus Notice: Undefined index: abstract_id in /afs/lama.univ-savoie.fr/user/httpd/html/sitelama/Membres/pages_web/types09/program.php on line 136 Notice: Undefined index: abstract_id in /afs/lama.univ-savoie.fr/user/httpd/html/sitelama/Membres/pages_web/types09/program.php on line 136
12:00 — Dulma Rodriguez Notice: Undefined index: abstract_id in /afs/lama.univ-savoie.fr/user/httpd/html/sitelama/Membres/pages_web/types09/program.php on line 123 Notice: Undefined index: abstract_id in /afs/lama.univ-savoie.fr/user/httpd/html/sitelama/Membres/pages_web/types09/program.php on line 123 — abstractslides
Efficient Type-Checking for Amortised Heap-Space Analysis Notice: Undefined index: abstract_id in /afs/lama.univ-savoie.fr/user/httpd/html/sitelama/Membres/pages_web/types09/program.php on line 136 Notice: Undefined index: abstract_id in /afs/lama.univ-savoie.fr/user/httpd/html/sitelama/Membres/pages_web/types09/program.php on line 136
12:30 — Lunch
14:00 — Damien Pous Notice: Undefined index: abstract_id in /afs/lama.univ-savoie.fr/user/httpd/html/sitelama/Membres/pages_web/types09/program.php on line 123 Notice: Undefined index: abstract_id in /afs/lama.univ-savoie.fr/user/httpd/html/sitelama/Membres/pages_web/types09/program.php on line 123 — abstractslides
Typing and Untyping Various Algebras Notice: Undefined index: abstract_id in /afs/lama.univ-savoie.fr/user/httpd/html/sitelama/Membres/pages_web/types09/program.php on line 136 Notice: Undefined index: abstract_id in /afs/lama.univ-savoie.fr/user/httpd/html/sitelama/Membres/pages_web/types09/program.php on line 136
14:30 — Francois Garillot Notice: Undefined index: abstract_id in /afs/lama.univ-savoie.fr/user/httpd/html/sitelama/Membres/pages_web/types09/program.php on line 123 Notice: Undefined index: abstract_id in /afs/lama.univ-savoie.fr/user/httpd/html/sitelama/Membres/pages_web/types09/program.php on line 123 — abstractslides
Working effectively with generic subgroups Notice: Undefined index: abstract_id in /afs/lama.univ-savoie.fr/user/httpd/html/sitelama/Membres/pages_web/types09/program.php on line 136 Notice: Undefined index: abstract_id in /afs/lama.univ-savoie.fr/user/httpd/html/sitelama/Membres/pages_web/types09/program.php on line 136
15:00 — Coffee Break
15:30 — Micaela Mayero Notice: Undefined index: abstract_id in /afs/lama.univ-savoie.fr/user/httpd/html/sitelama/Membres/pages_web/types09/program.php on line 123 Notice: Undefined index: abstract_id in /afs/lama.univ-savoie.fr/user/httpd/html/sitelama/Membres/pages_web/types09/program.php on line 123 — abstractslides
Certification of Numerical Analysis Programs Notice: Undefined index: abstract_id in /afs/lama.univ-savoie.fr/user/httpd/html/sitelama/Membres/pages_web/types09/program.php on line 136 Notice: Undefined index: abstract_id in /afs/lama.univ-savoie.fr/user/httpd/html/sitelama/Membres/pages_web/types09/program.php on line 136
16:00 — Barbara Petit Notice: Undefined index: abstract_id in /afs/lama.univ-savoie.fr/user/httpd/html/sitelama/Membres/pages_web/types09/program.php on line 123 Notice: Undefined index: abstract_id in /afs/lama.univ-savoie.fr/user/httpd/html/sitelama/Membres/pages_web/types09/program.php on line 123 — abstractslides
A lambda calculus with pattern matching and polymorphims Notice: Undefined index: abstract_id in /afs/lama.univ-savoie.fr/user/httpd/html/sitelama/Membres/pages_web/types09/program.php on line 136 Notice: Undefined index: abstract_id in /afs/lama.univ-savoie.fr/user/httpd/html/sitelama/Membres/pages_web/types09/program.php on line 136

Demos

Humayoun Muhammad
Mathematical Proofs in Natural Languages (MathNat)
Abstract: MathNat is a project for developing tools to enable automatic formalisation of mathematical text.
We proceed in two steps:
  1. Syntax: We develop a controlled language for mathematical text, mainly proofs by using a type theoretic approach. This is a subset of natural language.
  2. Semantics: We translate this controlled language to an abstract mathematical language (MathAbs). MathAbs is a system independent formal language for writing mathematics. We also solve some basic anaphora in this step.
In this demo, I will present the current status of MathNat development.
Vincent Laporte
Coq-GeoGebra interface
Abstract: This is a tool whose aim is to build and display a dynamic figure while a theorem of Euclidian geometry is proved. Based on Jean Duprat\'s formalization of this geometry in Coq, this tool is able to construct a figure from a proof context. Thanks to GeoGebra capabilities, the user is allowed to change the figure him or herself. Therefore this tool is also able to check a figure against the current context. Besides the figure evolves accordingly to the changes occurring in the proof context as the proof goes on. This interface has been designed so as to be extensible: it may easily take into account the modifications of the formalization. Moreover, its use might not be limited to this particular formalization of plane geometry.
Christophe Raffalli
PML
Abstract: I shall present the current status of PML development. Notably, the termination test implemented by Pierre Hyvernat.

Social Events

  • The volunteers may have an easy mountain walk in the afternoon on the 14th
  • The dinner on the 14th will have some regional dishes.