28532 articles – 22057 Notices  [english version]

hal-00647390, version 1

## Continuation-passing Style Models Complete for Intuitionistic Logic

Danko Ilik () a123

(2010)

Résumé : A class of models is presented, in the form of continuation monads polymorphic for first-order individuals, that is sound and complete for minimal intuitionistic predicate logic. The proofs of soundness and completeness are constructive and the computational content of their composition is, in particular, a $\beta$-normalisation-by-evaluation program for simply typed lambda calculus with sum types. Although the inspiration comes from Danvy's type-directed partial evaluator for the same lambda calculus, the there essential use of delimited control operators (i.e. computational effects) is avoided. The role of polymorphism is crucial -- dropping it allows one to obtain a notion of model complete for classical predicate logic. The connection between ours and Kripke models is made through a strengthening of the Double-negation Shift schema.

• a –  Polytechnique - X
• 1 :  Laboratoire d'informatique de l'école polytechnique (LIX)
• CNRS : UMR7161 – Polytechnique - X
• 2 :  PI.R2 (INRIA Paris - Rocquencourt)
• INRIA – Université Paris VII - Paris Diderot – CNRS : UMR7126
• 3 :  Preuves, Programmes et Systèmes (PPS)
• CNRS : UMR7126 – Université Paris VII - Paris Diderot

• hal-00647390, version 1
• oai:hal.inria.fr:hal-00647390
• Contributeur :
• Soumis le : Vendredi 2 Décembre 2011, 00:28:38
• Dernière modification le : Vendredi 2 Décembre 2011, 13:44:32