scientific article

Publication date: 17 September 1992

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

models type systems combinatory logic pure $\lambda $ -calculus

Introductory exposition (textbooks, tutorial papers, etc.) pertaining to computer science (68-01) Introductory exposition (textbooks, tutorial papers, etc.) pertaining to mathematical logic and foundations (03-01) Specification and verification (program logics, model checking, etc.) (68Q60) Abstract data types; algebraic specification (68Q65) General topics in the theory of software (68N01) Combinatory logic and lambda calculus (03B40) Computability and recursion theory on ordinals, admissible sets, etc. (03D60)

Related Items (76)

Classical logic, storage operators and second-order lambda-calculus ⋮ Pattern matching as cut elimination ⋮ Intersection types for explicit substitutions ⋮ Head linear reduction and pure proof net extraction ⋮ The differential $\lambda \mu$-calculus ⋮ The Inf function in the system $F$ ⋮ Intersection-types à la Church ⋮ Rétractions et interprétation interne du polymorphisme : le problème de la rétraction universelle ⋮ Unnamed Item ⋮ Unnamed Item ⋮ A conjecture on numeral systems ⋮ Execution time of λ-terms via denotational semantics and intersection types ⋮ Strong normalization and typability with intersection types ⋮ A completeness result for a realisability semantics for an intersection type system ⋮ Monoidal computer. I: Basic computability by string diagrams ⋮ Some properties of the -calculus ⋮ Subtyping + extensionality: Confluence of βηtop reduction in F≤ ⋮ Characterising Strongly Normalising Intuitionistic Sequent Terms ⋮ Machine Deduction ⋮ Entiers intuitionnistes et entiers classiques en $\lambda \, C$-calcul ⋮ The Scott model of linear logic is the extensional collapse of its relational model ⋮ Böhm theorem and Böhm trees for the $\varLambda \mu$-calculus ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Opérateurs de mise en mémoire et traduction de Gödel. (Storage operators and Gödel translation) ⋮ A fuzzy language. ⋮ On strong normalization and type inference in the intersection type discipline ⋮ Behavioural inverse limit $\lambda$-models ⋮ On phase semantics and denotational semantics in multiplicative-additive linear logic ⋮ λμ-calculus and Böhm's theorem ⋮ Filter models for conjunctive-disjunctive $\lambda$-calculi ⋮ Proving properties of typed $\lambda$-terms using realizability, covers, and sheaves ⋮ Lambda abstraction algebras: representation theorems ⋮ A new deconstructive logic: linear logic ⋮ On the concurrent computational content of intermediate logics ⋮ Krivine's classical realisability from a categorical perspective ⋮ Proofs of strong normalisation for second order classical natural deduction ⋮ Parameter-free polymorphic types ⋮ The Typed Böhm Theorem ⋮ Towards Lambda Calculus Order-Incompleteness ⋮ The vectorial $\lambda$-calculus ⋮ Résultats de complétude pour des classes de types du système $\mathcal {AF}2$ ⋮ Une réponse négative à la conjecture de E. Tronci pour les systèmes numériques typés ⋮ Logical equivalence for subtyping object and recursive types ⋮ Strong normalization from an unusual point of view ⋮ Constructive logics. I: A tutorial on proof systems and typed $\lambda$- calculi ⋮ A $\kappa$-denotational semantics for map theory in ZFC+SI ⋮ Unnamed Item ⋮ Les types de données syntaxiques du système ${\cal F}$ ⋮ Simplified Reducibility Proofs of Church-Rosser for β- and βη-reduction ⋮ LesI-types du système ${\cal F}$ ⋮ Cut-elimination in the strict intersection type assignment system is strongly normalizing ⋮ Full intersection types and topologies in lambda calculus ⋮ A completeness result for the simply typed $\lambda \mu $-calculus ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Strong storage operators and data types ⋮ Opérateurs de mise en mémoire et types $\forall $-positifs ⋮ The algebraic lambda calculus ⋮ An algebraic view of the Böhm-out technique ⋮ Building continuous webbed models for system F ⋮ A finite equational axiomatization of the functional algebras for the lambda calculus ⋮ Dedekind completion as a method for constructing new Scott domains ⋮ Strongly Normalising Cut-Elimination with Strict Intersection Types ⋮ Reducibility ⋮ Strong normalization property for second order linear logic ⋮ Compositional characterisations of $\lambda$-terms using intersection types ⋮ Typing untyped $\lambda$-terms, or reducibility strikes again! ⋮ Normalization without reducibility ⋮ From computation to foundations via functions and application: The $\lambda$-calculus and its webbed models ⋮ On the algebraic models of lambda calculus ⋮ Assertions, Hypotheses, Conjectures, Expectations: Rough-Sets Semantics and Proof Theory ⋮ Une Preuve Formelle et Intuitionniste du Théorème de Complétude de la Logique Classique ⋮ Set-theoretical and other elementary models of the $\lambda$-calculus ⋮ An equivalence between lambda- terms ⋮ Synthesis of ML programs in the system Coq

This page was built for publication: