Types in lambda calculi and programming languages
[For the entire collection see Zbl 0758.00013.] Type theory is still an active research area, and it is the moment of a general classification of the existing type systems on the basis of a common frame of reference. This is exactly what the authors do in this paper. The exposition concentrates on typed lambda calculi, although at many places the relations with programming languages are pointed out. We consider that the only thing we have to note is that the main classification criterion is based on the original ``implicit (H. B. Curry, 1934) and ``explicit (A. Church, 1941) typing systems, and then to refer to the more extensive work on the same subject due to the first author and \textit{W. Dekkers} [``Typed lambda calculi, syntax and semantics (to appear)].
- Algebraic domains of natural transformations
- A unified approach to type theory through a refined -calculus
- Some lambda calculus and type theory formalized
- Type Class Instances for Type-Level Lambdas in Haskell
- scientific article; zbMATH DE number 6496907 (Why is no real title available?)
- scientific article; zbMATH DE number 4002073 (Why is no real title available?)
- Simplified reducibility proofs of Church-Rosser for \({\beta}\)- and \({\beta}{\eta}\)-reduction
- Communicating contexts: A pragmatic approach to information exchange
- Comparing Hagino's categorical programming language and typed lambda- calculi
- Computational interpretations of linear logic
- Abstractions for multi-sorted substitutions
- Encoding of predicate subtyping with proof irrelevance in the -calculus modulo theory
- Translating lambda calculus into C++ templates
This page was built for publication: Types in lambda calculi and programming languages
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4038654)
