Typing and computational properties of lambda expressions

DOI10.1016/0304-3975(86)90109-XzbMath0613.68020OpenAlexW1968391490MaRDI QIDQ1819575

Daniel Leivant

Publication date: 1986

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0304-3975(86)90109-x

zbMATH Keywords

convergencenormalizabilitylambda calculussecond-order modelstypinglambda expressionssemantical properties

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Abstract data types; algebraic specification (68Q65) Combinatory logic and lambda calculus (03B40)

Related Items (12)

Intersection types for explicit substitutions ⋮ Singleton, union and intersection types for program extraction ⋮ Machine Deduction ⋮ Behavioural inverse limit \(\lambda\)-models ⋮ Intersection type assignment systems with higher-order algebraic rewriting ⋮ Approximation and normalization results for typeable term rewriting systems ⋮ AN EXTENSION OF AN AUTOMATED TERMINATION METHOD OF RECURSIVE FUNCTIONS ⋮ On automating the extraction of programs from proofs using product types ⋮ Preface to the special volume ⋮ Completeness of type assignment systems with intersection, union, and type quantifiers ⋮ Compositional characterisations of \(\lambda\)-terms using intersection types ⋮ Normalization without reducibility

Uses Software

• Automath

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• An extension of basic functionality theory for \(\lambda\)-calculus
• The lambda calculus, its syntax and semantics
• Functionals defined by recursion
• A proof of cut-elimination theorem in simple type-theory
• Combinators, \(\lambda\)-terms and proof theory
• A filter lambda model and the completeness of type assignment
• The Expressiveness of Simple and Second-Order Type Structures
• Functional Characters of Solvable Terms
• The Relation between Computational and Denotational Properties for Scott’s ${\text{D}}_\infty $-Models of the Lambda-Calculus
• Hauptsatz for higher order logic
• Intensional interpretations of functionals of finite type I
• Completeness and Hauptsatz for second order logic1
• A nonconstructive proof of Gentzen’s Hauptsatz for second order predicate logic
• Resolution in type theory
• Completeness in the theory of types

This page was built for publication: Typing and computational properties of lambda expressions