A canonical locally named representation of binding

DOI10.1007/S10817-011-9229-YMaRDI QIDQ2392482zbMATH OpenOpenAlexFDO

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

zbMATH Keywords

lambda calculusbindingformal proof

Mathematics Subject Classification ID

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

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

Cites work

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

Cited in

(15)

• Mechanizing metatheory without typing contexts
• External and internal syntax of the \(\lambda \)-calculus
• A formalized general theory of syntax with bindings: extended version
• The locally nameless representation
• Romeo: a system for more flexible binding-safe programming
• scientific article; zbMATH DE number 1149906 (Why is no real title available?)
• HOCore in Coq
• Term-generic logic
• Rensets and renaming-based recursion for syntax with bindings extended version
• 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
• Binding structures as an abstract data type
• Contextual equivalence for inductive definitions with binders in higher order typed functional programming
• scientific article; zbMATH DE number 89006 (Why is no real title available?)

Describes a project that uses

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)