The semantics of second-order lambda calculus

DOI10.1016/0890-5401(90)90044-IzbMath0714.68052OpenAlexW2052447934MaRDI QIDQ751294

Albert R. Meyer, John C. Mitchell, Kim B. Bruce

Publication date: 1990

Published in: Information and Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0890-5401(90)90044-i

zbMATH Keywords

typespolymorphic functionskindsScott's domains

Mathematics Subject Classification ID

Theory of programming languages (68N15) Semantics in the theory of computing (68Q55)

Related Items

\(F\)-semantics for type assignment systems, Categorical data types in parametric polymorphism, Semantics of the second order lambda calculus, Polymorphic extensions of simple type structures. With an application to a bar recursive minimization, Parametricity of extensionally collapsed term models of polymorphism and their categorical properties, Singleton, union and intersection types for program extraction, Monad transformers as monoid transformers, Denotational semantics as a foundation for cost recurrence extraction for functional languages, A domain-theoretic semantics of lax generic functions., The equivalence of two semantic definitions for inheritance in object-oriented languages, Types, abstraction, and parametric polymorphism, part 2, A modest model of records, inheritance, and bounded quantification, Between constructive mathematics and PROLOG, Recursive types for Fun, Categorical models of polymorphism, Constructing type systems over an operational semantics, Operations on records, Functorial polymorphism, CATEGORICAL MODEL CONSTRUCTION FOR PROVING SYNTACTIC PROPERTIES, Term-generic logic, A full continuous model of polymorphism, A paradigmatic object-oriented programming language: Design, static typing and semantics, CPO-models for second order lambda calculus with recursive types and subtyping, Polymorphic lambda calculus and subtyping.

Uses Software

• ML
• Ada95
• Automath
• ALGOL 60

Cites Work

• The lambda calculus. Its syntax and semantics. Rev. ed.
• Kripke-style models for typed lambda calculus
• The system \({\mathcal F}\) of variable types, fifteen years later
• The calculus of constructions
• Polymorphic type inference and containment
• CLU reference manual
• LCF considered as a programming language
• Fully abstract models of typed \(\lambda\)-calculi
• A theory of type polymorphism in programming
• The typed lambda-calculus is not elementary recursive
• Domain theoretic models of polymorphism
• The completeness theorem for typing lambda-terms
• Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
• Combinators, \(\lambda\)-terms and proof theory
• Effective operations on partial recursive functions
• Models of the lambda calculus
• A filter lambda model and the completeness of type assignment
• Recursive models for constructive set theories
• The Expressiveness of Simple and Second-Order Type Structures
• Semantics for classical AUTOMATH and related systems
• An ideal model for recursive polymorphic types
• On the Semantics of “Data Type”
• Data Types as Lattices
• What is a model of the lambda calculus?
• Correspondence between ALGOL 60 and Church's Lambda-notation
• Completeness in the theory of types
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item