Séminaire, Feb. 14, 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èsmidi. 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 socalled 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 orderincompleteness of lambda calculus, by studying the connection between the notion of absolute unorderability in a specific point and a weaker notion of subtractivity, namely nsubtractivity, for partially ordered algebras. Finally we study the relation between nsubtractivity 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 typetheory is becoming the standard way to formalize mathematics, at the same time as displacing traditional platforms for highinsurance programming.
However, current implementations of typetheory are not always satisfactory in the sense that some "obvious truth" are impossible to prove, making typetheory awkward to use for many applications, both in formalization and programming.
We propose an extension of typetheory with colored terms, a notion of color erasure, and an interpretation of colored types as predicates. That leads to a more powerful typetheory: Some proofs and definitions can now be trivially derived hence can be omitted; Beside, some parametricity results can be internalized. (Joint work with JeanPhilippe Bernardy.)
 15:30 – 16:30

Giulio Manzonetto (Université ParisNord)
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 BarendregtDekkersStatman'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.