A canonical locally named representation of binding

DOI10.1007/S10817-011-9229-YzbMATH Open1270.68073OpenAlexW2100730017MaRDI QIDQ2392482FDOQ2392482

Authors: Randy Pollack, Masahiko Sato, Wilmer Ricciotti 

Publication date: 1 August 2013

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10817-011-9229-y

Recommendations

• The locally nameless representation
• External and internal syntax of the \(\lambda \)-calculus
• Binding structures as an abstract data type
• A formalized general theory of syntax with bindings: extended version
• General bindings and alpha-equivalence in Nominal Isabelle

zbMATH Keywords

lambda calculusbindingformal proof

Mathematics Subject Classification ID

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

Cites Work

• Nominal techniques in Isabelle/HOL
• Untersuchungen über das logische Schliessen. I
• Nominal logic, a first order theory of names and binding
• Some lambda calculus and type theory formalized
• A framework for defining logics
• Title not available (Why is that?)
• Combinatory logic. With two sections by William Craig.
• Title not available (Why is that?)
• Mechanizing metatheory in a logical framework
• Title not available (Why is that?)
• Psi-calculi in Isabelle
• Engineering formal metatheory
• Substitution revisited
• Title not available (Why is that?)
• External and internal syntax of the \(\lambda \)-calculus
• The theory of contexts for first order and higher order abstract syntax
• Barendregt’s Variable Convention in Rule Inductions
• Title not available (Why is that?)
• Nominal Inversion Principles

Cited In (15)

• Rensets and renaming-based recursion for syntax with bindings
• Mechanizing metatheory without typing contexts
• A formalized general theory of syntax with bindings: extended version
• The locally nameless representation
• Romeo: a system for more flexible binding-safe programming
• External and internal syntax of the \(\lambda \)-calculus
• HOCore in Coq
• A unified treatment of syntax with binders
• Syntactic soundness proof of a type-and-capability system with hidden state
• Rensets and renaming-based recursion for syntax with bindings extended version
• Term-generic logic
• Title not available (Why is that?)
• Contextual equivalence for inductive definitions with binders in higher order typed functional programming
• Title not available (Why is that?)
• Binding structures as an abstract data type

Uses Software

• Isabelle/HOL
• Matita
• Twelf
• LEGO
• Nominal Isabelle
• Psi-calculi

This page was built for publication: A canonical locally named representation of binding

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2392482)