Two-level Lambda-calculus

DOI10.1016/j.entcs.2009.07.018zbMath1347.68051OpenAlexW1979665692MaRDI QIDQ4982628

Murdoch James Gabbay

Publication date: 9 April 2015

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

Full work available at URL: https://doi.org/10.1016/j.entcs.2009.07.018

zbMATH Keywords

confluencefunctional programminglambda calculusnominal termsmeta-variables

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Combinatory logic and lambda calculus (03B40)

Related Items (2)

Two-level nominal sets and semantic nominal terms: an extension of nominal set theory for handling meta-variables ⋮ The lambda-context calculus (extended version)

Uses Software

• Nominal Isabelle

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A new approach to abstract syntax with variable binding
• Capture-avoiding substitution as a nominal algebra
• Nominal unification
• Nominal rewriting
• A general mathematics of names
• Enriching the lambda calculus with contexts
• One-and-a-Halfth Order Terms: Curry-Howard and Incomplete Derivations
• One-and-a-halfth-order Logic
• Capture-Avoiding Substitution as a Nominal Algebra
• Curry-Style Types for Nominal Terms
• A Formal Calculus for Informal Equality with Binding
• Contextual modal type theory
• Computer Science Logic
• Logic Programming
• Automated Deduction – CADE-20
• A formulation of the simple theory of types
• A calculus of lambda calculus contexts
• A typed context calculus

This page was built for publication: Two-level Lambda-calculus