A Formalized Proof of Strong Normalization for Guarded Recursive Types

DOI10.1007/978-3-319-12736-1_8zbMath1453.68035OpenAlexW2148595046MaRDI QIDQ2789044

Andrea Vezzosi, Andreas Abel

Publication date: 26 February 2016

Published in: Programming Languages and Systems (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-319-12736-1_8

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Logic in computer science (03B70)

Related Items

Lewis meets Brouwer: constructive strict implication, POPLMark reloaded: Mechanizing proofs by logical relations, The Guarded Lambda-Calculus: Programming and Reasoning with Guarded Recursion for Coinductive Types, Unnamed Item, Guarded cubical type theory

Uses Software

• Agda