Monotone (co)inductive types and positive fixed-point types
Monotone (co)inductive types and positive fixed-point types
We study five extensions of the polymorphically typed lambda-calculus (system F) by type constructs intended to model fixed-points of monotone operators. Building on work by Geuvers concerning the relation between term rewrite systems for least pre-fixed-points and greatest post-fixed-points of positive type schemes (i.e., non-nested positive inductive and coinductive types) and so-called retract types, we show that there are reduction-preserving embeddings even between systems of monotone (co)inductive...
Natural deduction and sequent typed lambda calculus.
Natural Numbers In Illative Combinatory Logic.
Nondeterminism and fully abstract models
Normal forms in the typed -calculus with tuple types
Normalisation of the theory of Cartesian closed categories and conservativity of extensions of
Normalisation of the Theory T of Cartesian Closed Categories and Conservativity of Extensions T[x] of T
Using an inductive definition of normal terms of the theory of Cartesian Closed Categories with a given graph of distinguished morphisms, we give a reduction free proof of the decidability of this theory. This inductive definition enables us to show via functional completeness that extensions of such a theory by new constants (“indeterminates”) are conservative.
On a logical formalization of natural language
On Semantics of a Term Calculus for Classical Logic
Opérateurs de mise en mémoire et types -positifs
Point-fixe sur un ensemble restreint
Polyadic algebras over nonclassical logics
The polyadic algebras that arise from the algebraization of the first-order extensions of a SIC are characterized and a representation theorem is proved. Standard implicational calculi (SIC)'s were considered by H. Rasiowa [19] and include classical and intuitionistic logic and their various weakenings and fragments, the many-valued logics of Post and Łukasiewicz, modal logics that admit the rule of necessitation, BCK logic, etc.
Pre-adjunctions and lambda-algebraic theories
Predicate calculus and naive set theory in pure combinatory logic.
Predicate calculus of arbitrarily high finite order.
Présentation de la logique combinatoire en vue de ses applications
Probabilistic operational semantics for the lambda calculus
Probabilistic operational semantics for a nondeterministic extension of pure λ-calculus is studied. In this semantics, a term evaluates to a (finite or infinite) distribution of values. Small-step and big-step semantics, inductively and coinductively defined, are given. Moreover, small-step and big-step semantics are shown to produce identical outcomes, both in call-by-value and in call-by-name. Plotkin’s CPS translation is extended to accommodate the choice operator and shown correct with respect...
Probabilistic operational semantics for the lambda calculus
Probabilistic operational semantics for a nondeterministic extension of pure λ-calculus is studied. In this semantics, a term evaluates to a (finite or infinite) distribution of values. Small-step and big-step semantics, inductively and coinductively defined, are given. Moreover, small-step and big-step semantics are shown to produce identical outcomes, both in call-by-value and in call-by-name. Plotkin’s CPS translation is extended to accommodate the choice operator and shown correct with respect...
Probabilistic operational semantics for the lambda calculus
Probabilistic operational semantics for a nondeterministic extension of pure λ-calculus is studied. In this semantics, a term evaluates to a (finite or infinite) distribution of values. Small-step and big-step semantics, inductively and coinductively defined, are given. Moreover, small-step and big-step semantics are shown to produce identical outcomes, both in call-by-value and in call-by-name. Plotkin’s CPS translation is extended to accommodate the choice operator and shown correct with respect...