This paper gives a characterisation, via intersection types, of the strongly normalising terms of an intuitionistic sequent calculus (where LJ easily embeds). The soundness of the ...
This paper presents a new proof language for the Coq proof assistant. This language uses the declarative style. It aims at providing a simple, natural and robust alternative to the...
We present a procedure for computing normal forms of terms in Abadi and Cardelli’s functional object calculus. Even when equipped with simple types, terms of this calculus are no...
Abstract. Proof erasure plays an essential role in the paradigm of programming with theorem proving. In this paper, we introduce a form of attributive types that carry an attribute...
Abstract. We propose syntax and semantics for systems of intuitionistic and classical first order dependently sorted logic, with and withlity, retaining type dependency, but other...
We consider propositional formulas built on implication. The size of a formula is the number of occurrences of variables in it. We assume that two formulas which differ only in th...