A Realizability Model for Impredicative Hoare Type Theory
No abstract available.
Related papers
- Integrating Linear and Dependent Types POPL 2015
- Impredicative Observational Equality POPL 2023
- A reasonably exceptional type theory ICFP 2019
- Generic derivation of induction for impredicative encodings in Cedille CPP 2018
- Qualified types for MLF ICFP 2005
- Abstract Predicates and Mutable ADTs in Hoare Type Theory ESOP 2007
- Mechanized logical relations for termination-insensitive noninterference POPL 2021
- Polymorphism and separation in hoare type theory ICFP 2006