Proof-Relevant Logical Relations for Name Generation
From MaRDI portal
Publication:4637685
DOI10.23638/LMCS-14(1:25)2018zbMath1459.68041arXiv1708.05193OpenAlexW176593450MaRDI QIDQ4637685
Vivek Nigam, Martin Hofmann, Nick Benton
Publication date: 25 April 2018
Published in: Lecture Notes in Computer Science (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/1708.05193
Theory of programming languages (68N15) Functional programming and lambda calculus (68N18) Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Related Items (2)
Factorisation systems for logical relations and monadic lifting in type-and-effect system semantics ⋮ Deciding contextual equivalence of \(\nu \)-calculus with effectful contexts
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- A new approach to abstract syntax with variable binding
- On a monadic semantics for freshness
- Setoids in type theory
- FreshML
- Relational Reasoning for Recursive Types and References
- Reading, Writing and Relations
- Abstract effects and proof-relevant logical relations
- Typed Lambda Calculi and Applications
This page was built for publication: Proof-Relevant Logical Relations for Name Generation