Correlating Oracles

Thibaut Girka 1, 2, 3 Yann Régis-Gianas 2
2 PI.R2 - Design, study and implementation of languages for proofs and programs
Inria de Paris, CNRS - Centre National de la Recherche Scientifique, UPD7 - Université Paris Diderot - Paris 7, PPS - Preuves, Programmes et Systèmes
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/
Document type :
Software
Liste complète des métadonnées

Browse

- Identifier : swh:1:rev:cccf789c12617208fe188ad3dbc2746d4c884ab7  Browse

https://hal.inria.fr/hal-01831369
Contributor : Thibaut Girka <>
Submitted on : Saturday, July 14, 2018 - 10:31:47 PM
Last modification on : Wednesday, February 6, 2019 - 11:26:02 AM

Collections

Citation

Thibaut Girka, Yann Régis-Gianas. Correlating Oracles. 2018, 〈swh:1:rev:cccf789c12617208fe188ad3dbc2746d4c884ab7〉. 〈hal-01831369v2〉

Share

Metrics

Record views

136

Files downloads

74