Encoding abstract syntax without fresh names

<a class="pub-badge pub-badge--doi" href="https://doi.org/10.1007/S10817-011-9220-7" rel="nofollow">DOI 10.1007/S10817-011-9220-7</a><a class="pub-badge pub-badge--grey" href="https://zbmath.org/1269.68043" rel="nofollow">zbMATH</a><a class="pub-badge pub-badge--grey" href="https://openalex.org/works/W2074694595" rel="nofollow">OpenAlex</a><a class="pub-badge pub-badge--mardi" href="https://portal.mardi4nfdi.de/wiki/Item:Q2392477" rel="nofollow">MaRDI QID Q2392477</a><a class="pub-badge pub-badge--grey" href="https://fdo.portal.mardi4nfdi.de/fdo/Q2392477" rel="nofollow">FDO</a>

Authors Matthew R. Lakin, Andrew M. Pitts

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-9220-7

zbMATH Keywords

meta-programmingalpha-equivalencenominal abstract syntax

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Semantics in the theory of computing (68Q55)

Recommendations

• scientific article; zbMATH DE number 1612495
• FreshML: programming with binders made simple
• Alpha-structural recursion and induction
• Foundations of nominal techniques: logic and semantics of variables in abstract syntax
• scientific article; zbMATH DE number 2242589

Cites work

• scientific article; zbMATH DE number 2090728 (Why is no real title available?)
• scientific article; zbMATH DE number 3400430 (Why is no real title available?)
• A new approach to abstract syntax with variable binding
• Alpha-structural recursion and induction
• Automata, Languages and Programming
• Capture-avoiding substitution as a nominal algebra
• Equivalence in functional languages with effects
• Generative Unbinding of Names
• Logic Programming
• Logical frameworks
• Multi-paradigm Declarative Languages
• Nominal techniques in Isabelle/HOL
• Nominal unification
• On a monadic semantics for freshness
• Operational equivalences for untyped and polymorphic object calculi
• Ott, effective tool support for the working semanticist
• Proving congruence of bisimulation in functional programming languages
• Relational reasoning about contexts
• Resolving Inductive Definitions with Binders in Higher-Order Typed Functional Programming
• Term Rewriting and Applications
• The lambda calculus. Its syntax and semantics. Rev. ed.
• The revised report on the syntactic theories of sequential control and state
• The semantics of constraint logic programs1Note that reviewing of this paper was handled by the Editor-in-Chief.1
• The undecidability of the second-order unification problem
• Typed Lambda Calculi and Applications

Cited in

(1)

• Contextual equivalence for inductive definitions with binders in higher order typed functional programming

Describes a project that uses

Uses Software

• Ott
• ML
• Nominal Isabelle

This page was built for publication: Encoding abstract syntax without fresh names

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