Correlating Oracles - Archive ouverte HAL Access content directly
Software Year :

Correlating Oracles

(1, 2, 3) , (2)
1
2
3

Abstract

This archive contains the Coq development described in the paper “Verifiable Semantic Difference Languages”[1]. It is composed of meta-theoritical definitions and proofs (coq/OracleLanguage.v, coq/ProgrammingLanguage.v, …) as well as an instantiation of those definitions on a toy imperative language (coq/Imp/). [1]: https://hal.inria.fr/hal-01653283/
142 View
26 Download

Share

Gmail Facebook Twitter LinkedIn More