Encoding abstract syntax without fresh names

DOI10.1007/S10817-011-9220-7zbMATH Open1269.68043OpenAlexW2074694595MaRDI QIDQ2392477FDOQ2392477

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

Recommendations

• Publication:2721104
• 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

zbMATH Keywords

meta-programmingalpha-equivalencenominal abstract syntax

Mathematics Subject Classification ID

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

Cites Work

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

Cited In (1)

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

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)