Sciweavers

CSL
2005
Springer
14 years 5 months ago
Light Functional Interpretation
We give a Natural Deduction formulation of an adaptation of G¨odel’s functional (Dialectica) interpretation to the extraction of (more) efficient programs from (classical) proof...
Mircea-Dan Hernest
LFCS
2007
Springer
14 years 5 months ago
The Intensional Lambda Calculus
We introduce a natural deduction formulation for the Logic of Proofs, a refinement of modal logic S4 in which the assertion PA is replaced by [[s]]A whose intended reading is “s...
Sergei N. Artëmov, Eduardo Bonelli