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

Carte non disponible
Speaker Home page :
Speaker :
Speaker Affiliation :

()

Date/heure
Date(s) - 03/03/2016
11 h 00 min - 12 h 00 min

Catégories


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.

http://pauillac.inria.fr/~herbelin/


Retour en haut 

Secured By miniOrange