Skip to content

Use the persistent function space in logical relations and add the symbol table example

Amin Timany requested to merge ci/amin/logrel-update into master
  • Use persistence relations for both the unary and binary logical relation
  • Extend the language and type system with existential and universal quantifiers, and the FAA operation.
  • Separate the proofs of the compatiblity lemmas
  • Add the proof of the symbol table from Derek's talk
  • Make the logical relation an iProp (it was a Prop)
Edited by Ralf Jung

Merge request reports