230 search results - page 1 / 46 » Completing Herbelin's Programme |
TLCA
2007
Springer
13 years 10 months ago
2007
Springer
Abstract. In 1994 Herbelin started and partially achieved the programme of showing that, for intuitionistic implicational logic, there is a Curry-Howard interpretation of sequent c...
WOLLIC
2009
Springer
13 years 11 months ago
2009
Springer
We give a simple intuitionistic completeness proof of Kripke semantics with constant domain for intuitionistic logic with implication and universal quantification. We use a cut-fr...
APAL
2010
13 years 4 months ago
2010
We introduce a notion of Kripke model for classical logic for which we constructively prove soundness and cut-free completeness. We discuss the meaning of the new notion and its a...
ESOP
2012
Springer
12 years 6 days ago
2012
Springer
Abstract. A behavioral contract in a higher-order language may invoke methods of unknown objects. Although this expressive power allows programmers to formulate sophisticated contr...
FOSSACS
2010
Springer
13 years 11 months ago
2010
Springer
Λµ-calculus was introduced as a Böhm-complete extension of Parigot's λµ-calculus. Λµ-calculus, contrarily to Parigot's calculus, is a calculus of CBN delimited con...