Proof-Relevant Logical Relations for Name Generation

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

zbMATH Keywords

program transformationlogical relationsparametricity

Mathematics Subject Classification ID

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

• Freshml

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