A ...-calculus with an algorithmic ... .
A new type assignment for ...-terms.
A one axiom set theory based on higher order predicate calculus.
A Parigot-style linear -calculus for full intuitionistic linear logic.
An intensional approach to questions
Axiomatisation des manipulations symboliques en calcul des prédicats
Beta-reduction as unification
We define a new unification problem, which we call β-unification and which can be used to characterize the β-strong normalization of terms in the λ-calculus. We prove the undecidability of β-unification, its connection with the system of intersection types, and several of its basic properties.
Bibliographie commentée
Categorical, functorial and algebraic aspects of the type-free lambda calculus
Category theory based on combinatory logic.
Combinatory logic and the ω-rule
Complexité de la réduction en logique combinatoire
Complexity of -term reductions
Computational Interrpretations of Logics
CPO-models for second order lambda calculus with recursive types and subtyping
Data types as lattices : retractions, closures and projections
De la notion d'opération à celle d'opérateur ou à la recherche de formalismes intrinsèques
Deciding inclusion of set constants over infinite non-strict data structures
Various static analyses of functional programming languages that permit infinite data structures make use of set constants like Top, Inf, and Bot, denoting all terms, all lists not eventually ending in Nil, and all non-terminating programs, respectively. We use a set language that permits union, constructors and recursive definition of set constants with a greatest fixpoint semantics in the set of all, also infinite, computable trees, where all term constructors are non-strict. This...
...-definable functionals and ... Conversion.
...-definierbare Funktionen auf Peanoalgebren.