The semantics of second-order lambda calculus
From MaRDI portal
The second-order lambda calculus, as a tool for solving problems connected with polymorphisms, can become important with respect to some programming languages. Because of its explicit lambda abstraction over types this calculus cannot be interpreted in the standard (naive) way, where terms denote functions and types sets of functions. The authors, inspired by some preceding ideas (Girard, Reynolds, McCracken, indeed Scott), define two model concepts: environmental model and combinatory model. The equivalence of both the models is proved as well as many other theorems and lemmas. A comparison with other models is given and some open problems are formulated.
Recommendations
- Semantics of the second order lambda calculus
- scientific article; zbMATH DE number 3882403
- scientific article; zbMATH DE number 4051568
- An elementary fragment of second-order lambda calculus
- On the semantics of second order lambda calculus: From bruce-meyer-mitchell models to hyperdoctrine models and vice-versa
- scientific article; zbMATH DE number 4051567
- Semantics of linear/modal lambda calculus
- scientific article; zbMATH DE number 6148924
- RPO, Second-order Contexts, and Lambda-calculus
- The Intensional Lambda Calculus
Cites work
- A filter lambda model and the completeness of type assignment
- A theory of type polymorphism in programming
- An ideal model for recursive polymorphic types
- CLU reference manual
- Combinators, \(\lambda\)-terms and proof theory
- Completeness in the theory of types
- Correspondence between ALGOL 60 and Church's Lambda-notation
- Data Types as Lattices
- Domain theoretic models of polymorphism
- Effective operations on partial recursive functions
- Fully abstract models of typed \(\lambda\)-calculi
- scientific article; zbMATH DE number 4180771 (Why is no real title available?)
- scientific article; zbMATH DE number 3882403 (Why is no real title available?)
- scientific article; zbMATH DE number 3882404 (Why is no real title available?)
- scientific article; zbMATH DE number 3854400 (Why is no real title available?)
- scientific article; zbMATH DE number 3890703 (Why is no real title available?)
- scientific article; zbMATH DE number 3902022 (Why is no real title available?)
- scientific article; zbMATH DE number 3928328 (Why is no real title available?)
- scientific article; zbMATH DE number 3941503 (Why is no real title available?)
- scientific article; zbMATH DE number 4027427 (Why is no real title available?)
- scientific article; zbMATH DE number 4049849 (Why is no real title available?)
- scientific article; zbMATH DE number 3485174 (Why is no real title available?)
- scientific article; zbMATH DE number 3521951 (Why is no real title available?)
- scientific article; zbMATH DE number 3550165 (Why is no real title available?)
- scientific article; zbMATH DE number 3550662 (Why is no real title available?)
- scientific article; zbMATH DE number 3216998 (Why is no real title available?)
- scientific article; zbMATH DE number 3290336 (Why is no real title available?)
- scientific article; zbMATH DE number 3291134 (Why is no real title available?)
- Kripke-style models for typed lambda calculus
- LCF considered as a programming language
- Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
- Models of the lambda calculus
- On the Semantics of “Data Type”
- Polymorphic type inference and containment
- Recursive models for constructive set theories
- Semantics for classical AUTOMATH and related systems
- The calculus of constructions
- The completeness theorem for typing lambda-terms
- The Expressiveness of Simple and Second-Order Type Structures
- The lambda calculus. Its syntax and semantics. Rev. ed.
- The system \({\mathcal F}\) of variable types, fifteen years later
- The typed lambda-calculus is not elementary recursive
- What is a model of the lambda calculus?
Cited in
(34)- Between constructive mathematics and PROLOG
- Recursive types for Fun
- Categorical models of polymorphism
- Constructing type systems over an operational semantics
- \(F\)-semantics for type assignment systems
- A domain-theoretic semantics of lax generic functions.
- Polymorphic lambda calculus and subtyping.
- Typing and computational properties of lambda expressions
- A full continuous model of polymorphism
- Polymorphic extensions of simple type structures. With an application to a bar recursive minimization
- Term-generic logic
- Counterpart semantics for a second-order -calculus
- CPO-models for second order lambda calculus with recursive types and subtyping
- scientific article; zbMATH DE number 3882403 (Why is no real title available?)
- Operations on records
- Semantics for classical AUTOMATH and related systems
- One method of defining the semantics of programming language constructs in terms of lambda calculus. II
- scientific article; zbMATH DE number 4051567 (Why is no real title available?)
- scientific article; zbMATH DE number 4051568 (Why is no real title available?)
- Semantics of the second order lambda calculus
- Categorical data types in parametric polymorphism
- Toward a semantics for the QUEST language
- scientific article; zbMATH DE number 218500 (Why is no real title available?)
- A paradigmatic object-oriented programming language: Design, static typing and semantics
- Parametricity of extensionally collapsed term models of polymorphism and their categorical properties
- Singleton, union and intersection types for program extraction
- On the semantics of second order lambda calculus: From bruce-meyer-mitchell models to hyperdoctrine models and vice-versa
- Denotational semantics as a foundation for cost recurrence extraction for functional languages
- CATEGORICAL MODEL CONSTRUCTION FOR PROVING SYNTACTIC PROPERTIES
- The equivalence of two semantic definitions for inheritance in object-oriented languages
- Monad transformers as monoid transformers
- Types, abstraction, and parametric polymorphism, part 2
- Functorial polymorphism
- A modest model of records, inheritance, and bounded quantification
This page was built for publication: The semantics of second-order lambda calculus
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q751294)
