A metalanguage for programming with bound names modulo renaming

DOI10.1007/10722010_15MaRDI QIDQ2721104zbMATH OpenFDO

Authors Andrew M. Pitts, Murdoch J. Gabbay

Publication date 1 July 2001

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/10722010_15

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• Meta-programming with names and necessity
• A metalanguage for guarded iteration
• A metalanguage for guarded iteration
• A metalogic programming approach: language, semantics and applications
• SEMANTICS OF A METALOGIC PROGRAMMING LANGUAGE
• scientific article; zbMATH DE number 1956524
• A proof dedicated meta-language

Cited in

(26)

• A study of substitution, using nominal techniques and Fraenkel-Mostowksi sets
• The lambda-context calculus (extended version)
• Binding operators for nominal sets
• Coalgebraic minimization of HD-automata for the -calculus using polymorphic types
• Nominal logic, a first order theory of names and binding
• Mechanized metatheory revisited
• Encoding abstract syntax without fresh names
• A survey of strategies in rule-based program transformation systems
• Nominal syntax with atom substitutions
• A simple nominal type theory
• A survey of rewriting strategies in program transformation systems
• Manipulating trees with hidden labels
• Contextual equivalence for inductive definitions with binders in higher order typed functional programming
• Generative unbinding of names
• Generative Unbinding of Names
• Validating Brouwer's continuity principle for numbers using named exceptions
• A fresh look at programming with names and binders
• FreshML: programming with binders made simple
• A dependent type theory with abstractable names
• Denotational semantics with nominal Scott domains
• A metalanguage for guarded iteration
• Relating state-based and process-based concurrency through linear logic (full-version)
• Formal compiler construction in a logical framework
• An initial algebra approach to term rewriting systems with variable binders
• A polynomial nominal unification algorithm
• Matching and alpha-equivalence check for nominal terms

Describes a project that uses

Uses Software

• HOL

This page was built for publication: A metalanguage for programming with bound names modulo renaming

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