Nominal system T

DOI10.1145/1706299.1706321MaRDI QIDQ5255070zbMATH OpenOpenAlexFDO

Authors Andrew M. Pitts

Publication date 11 June 2015

Published in Proceedings of the 37th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/1706299.1706321

zbMATH Keywords

alpha-equivalencebindersrecursiontypes

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• scientific article; zbMATH DE number 3333262
• Extended T-systems
• scientific article; zbMATH DE number 1390279
• Nominal rewriting
• Typed nominal rewriting
• Computer Science Logic
• Nominal unification
• Nominal Renaming Sets

Cited in

(7)

• Alpha-structural induction and recursion for the lambda calculus in constructive type theory
• Formalizing adequacy: a case study for higher-order abstract syntax
• Structural recursion with locally scoped names
• Principal types for nominal theories
• Binding in nominal equational logic
• A Recursion Combinator for Nominal Datatypes Implemented in Isabelle/HOL
• Validating Brouwer's continuity principle for numbers using named exceptions

This page was built for publication: Nominal system T

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