Skip to Main content Skip to Navigation

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
UPD7 - Université Paris Diderot - Paris 7, CNRS - Centre National de la Recherche Scientifique, IRIF (UMR_8243) - Institut de Recherche en Informatique Fondamentale, Inria de Paris
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/
Document type :
Software
Complete list of metadata

Browse

Present sur SoftwareHeritage
swh:1:dir:2c01e745c6d89e0eeb9a6ec9590f7ef0750b7002;origin=https://hal.archives-ouvertes.fr/hal-01831369;visit=swh:1:snp:42f0897956e700a23f5b8aafce43360b8699c0f1;anchor=swh:1:rev:698771f9ca7ce7605fdcabf27b5851f322ea692c;path=/

https://hal.inria.fr/hal-01831369
Contributor : Thibaut Girka Connect in order to contact the contributor
Submitted on : Saturday, July 14, 2018 - 10:31:47 PM
Last modification on : Friday, April 10, 2020 - 5:28:06 PM

Share

Metrics

Record views

202

Files downloads

342