Preuves, Programmes et Systèmes

Jeudi 2/7, Naohiko Hoshino (RIMS, Kyoto)

Linearization of realizability

For every PCA (partial combinatory algebra), we can construct categories such as effective toposes, assemblies and PERs (partial equivalence relations). They provide models of polymorphic lambda calculus and dependent type theory. In this talk, we consider linearlization of constructions of these categories. Instead of PCA, we consider an algebra that is a slight generalization of Abramsky's linear combinatory algebra (LCA) and observe that construction of assembiles and PER works well. On the other hand, it appears that the linearization of the construction of an effective topos from a tripos, called the Set(p) construction, does not work.