Séminaire, 14 février 2013
Cette journée Chocola sera suivie d'une rencontre du Groupe de travail Geocal du GDR IM, le 15 février.
Lieu
La rencontre aura lieu à l'École Normale Supérieure de Lyon, campus Jacques Monod, en salle des examens le matin, en amphi B l'après-midi. Pour venir, voir les instructions sur le site du LIP ou sur un plan, par exemple chez Google Maps. À l'entrée, se présenter à la réception, qui aura la liste des inscrits.
Programme
- 10:30 – 12:00
-
Antonino Salibra (Università Cà Foscari, Venezia, Italy)
Answering a question by Honsell and Plotkin, we show that there are two equations between lambda terms, the so-called subtractive equations, consistent with lambda calculus but not contemporaneously satisfied in any Scott continuous model.
We also relate the subtractive equations to the open problem of the order-incompleteness of lambda calculus, by studying the connection between the notion of absolute unorderability in a specific point and a weaker notion of subtractivity, namely n-subtractivity, for partially ordered algebras. Finally we study the relation between n-subtractivity and relativized separation conditions in topological algebras, obtaining an incompleteness theorem for a general topological semantics of lambda calculus.
- 14:00 – 15:00
-
Guilhem Moulin (Chalmers, Sweden)
Dependent type-theory is becoming the standard way to formalize mathematics, at the same time as displacing traditional platforms for high-insurance programming.
However, current implementations of type-theory are not always satisfactory in the sense that some "obvious truth" are impossible to prove, making type-theory awkward to use for many applications, both in formalization and programming.
We propose an extension of type-theory with colored terms, a notion of color erasure, and an interpretation of colored types as predicates. That leads to a more powerful type-theory: Some proofs and definitions can now be trivially derived hence can be omitted; Beside, some parametricity results can be internalized. (Joint work with Jean-Philippe Bernardy.)
- 15:30 – 16:30
-
Giulio Manzonetto (Université Paris-Nord)
In simply typed λ-calculus with one ground type the following theorem due to Loader holds. (i) Given the full model F over a finite set, the question whether some element f∈F is λ-definable is undecidable. In the λ-calculus with intersection types based on countably many atoms, the following is proved by Urzyczyn. (ii) It is undecidable whether a type is inhabited. Both statements are major results presented in Barendregt-Dekkers-Statman'12. We show that (i) and (ii) follow from each other in a natural way, by interpreting intersection types as continuous functions logically related to elements of F. From this, and a result by Joly on λ-definability, we get that Urzyczyn's theorem already holds for intersection types with at most two atoms.
