Categorical abstract machines for higher-order typed \(\lambda\)-calculi

DOI10.1016/0304-3975(94)00125-3zbMath0874.68029OpenAlexW2065588545MaRDI QIDQ1349667

Eike Ritter

Publication date: 27 February 1997

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

Full work available at URL: https://doi.org/10.1016/0304-3975(94)00125-3

Mathematics Subject Classification ID

Theory of programming languages (68N15) Closed categories (closed monoidal and Cartesian closed categories, etc.) (18D15) Combinatory logic and lambda calculus (03B40)

Related Items

Fibrational modal type theory, Reflection of formal tactics in a deductive reflection framework, Internal type theory

Uses Software

• LEGO

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• An abstract framework for environment machines
• The categorical abstract machine
• The calculus of constructions
• Type checking with universes
• Proof of termination of the rewriting system SUBSET on CCL
• Strong normalization of substitutions
• Categorical semantics for higher order polymorphic lambda calculus
• Explicit substitutions