Localisation

Adresses

Aix-Marseille Université
Institut de Mathématiques de Marseille (I2M) - UMR 7373
Site Saint-Charles : 3 place Victor Hugo, Case 19, 13331 Marseille Cedex 3
Site Luminy : Campus de Luminy - Case 907 - 13288 Marseille Cedex 9

Séminaire

dPAω: a dependently-typed classical arithmetic in finite types which proves dependent choices

Hugo Herbelin
INRIA, Rocquencourt-Paris
http://pauillac.inria.fr/~herbelin/

Date(s) : 03/03/2016   iCal
11h00 - 12h00

We extend classical arithmetic in finite types with an intuitionistically-restricted form of strong projection of existential quantification. In this system, by turning countable universal quantification into an infinite tuple, we can give a proof of the axiom of dependent choices.
All constructions of the system are computational, hence providing with a proof-as-program interpretation of dPAω. The presence of infinite tuples requires however to rely on a lazy evaluation strategy.

Catégories


Secured By miniOrange