Formal metatheory of the lambda calculus using Stoughton's substitution
From MaRDI portal
Publication:2358702
DOI10.1016/j.tcs.2016.08.025zbMath1383.03021MaRDI QIDQ2358702
Nora Szasz, Álvaro Tasistro, Ernesto Copello
Publication date: 15 June 2017
Published in: Theoretical Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.tcs.2016.08.025
03B40: Combinatory logic and lambda calculus
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Formalisation in constructive type theory of Stoughton's substitution for the lambda calculus
- A new approach to abstract syntax with variable binding
- The lambda calculus. Its syntax and semantics. Rev. ed.
- Nominal techniques in Isabelle/HOL
- Substitution revisited
- A formalised first-order confluence proof for the \(\lambda\)-calculus using one-sorted variable names.
- Alpha-structural induction and recursion for the lambda calculus in constructive type theory
- Nominal logic, a first order theory of names and binding
- The locally nameless representation
- Some lambda calculus and type theory formalized
- Foundations of Nominal Techniques: Logic and Semantics of Variables in Abstract Syntax
- Engineering formal metatheory
- Alpha-structural recursion and induction
- Parallel reductions in \(\lambda\)-calculus