A typed context calculus

DOI10.1016/S0304-3975(00)00174-2zbMath0989.68017OpenAlexW2113696254MaRDI QIDQ5958759

M. Hashimoto, Atsushi Ohori

Publication date: 3 March 2002

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

Full work available at URL: https://doi.org/10.1016/s0304-3975(00)00174-2

zbMATH Keywords

type systemalpha-renamingcontextlambda-calculus

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18)

Related Items

Nominal unification, An initial algebra approach to term rewriting systems with variable binders, A lambda-calculus for dynamic binding, Dynamic rebinding for marshalling and update, via redex-time and destruct-time reduction, Curry-Howard for incomplete first-order logic derivations using one-and-a-half level terms, Two-level Lambda-calculus, Processes against tests: on defining contextual equivalences, The lambda-context calculus (extended version), Functional Programming With Higher-order Abstract Syntax and Explicit Substitutions

Uses Software

• ML
• Modula

Cites Work

• A theory of binding structures and applications to rewriting
• A lambda-calculus for dynamic binding
• LCF considered as a programming language
• Fully abstract models of typed \(\lambda\)-calculi
• Higher order unification via explicit substitutions
• Enriching the lambda calculus with contexts
• Explicit substitutions
• Context rewriting
• Parallel reductions in \(\lambda\)-calculus
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item