untitled
<OAI-PMH schemaLocation=http://www.openarchives.org/OAI/2.0/ http://www.openarchives.org/OAI/2.0/OAI-PMH.xsd>
<responseDate>2018-01-15T18:30:37Z</responseDate>
<request identifier=oai:HAL:hal-01126128v1 verb=GetRecord metadataPrefix=oai_dc>http://api.archives-ouvertes.fr/oai/hal/</request>
<GetRecord>
<record>
<header>
<identifier>oai:HAL:hal-01126128v1</identifier>
<datestamp>2017-12-21</datestamp>
<setSpec>type:COMM</setSpec>
<setSpec>subject:info</setSpec>
<setSpec>collection:UNIV-AG</setSpec>
<setSpec>collection:CNAM</setSpec>
</header>
<metadata><dc>
<publisher>HAL CCSD</publisher>
<title lang=en>CoqInE : Translating the calculus of inductive constructions into the ??-calculus modulo.</title>
<creator>Boespflug, Mathieu</creator>
<creator>Burel, Guillaume</creator>
<contributor>Laboratoire Hydreco ; Université des Antilles et de la Guyane (UAG)</contributor>
<contributor>Centre d'Etude et De Recherche en Informatique du Cnam (CEDRIC) ; Conservatoire National des Arts et Métiers [CNAM] (CNAM)</contributor>
<source>Second International Workshop on Proof Exchange for Theorem Proving (PXTP 2012)</source>
<coverage>Manchester, United Kingdom</coverage>
<identifier>hal-01126128</identifier>
<identifier>https://hal.archives-ouvertes.fr/hal-01126128</identifier>
<source>https://hal.archives-ouvertes.fr/hal-01126128</source>
<source>Second International Workshop on Proof Exchange for Theorem Proving (PXTP 2012), Jun 2012, Manchester, United Kingdom</source>
<language>en</language>
<subject lang=en>proof translation,universal proof language,inductive types,dependant types,rewriting</subject>
<subject lang=fr>traduction de preuve,langage universel de preuves,types inductifs,types de personne à charge,réécriture</subject>
<subject>[INFO] Computer Science [cs]</subject>
<subject>[INFO.INFO-PL] Computer Science [cs]/Programming Languages [cs.PL]</subject>
<type>info:eu-repo/semantics/conferenceObject</type>
<type>Conference papers</type>
<description lang=en>We show how to translate the Calculus of Inductive Constructions (CIC) as implemented by Coq into the ??-calculus modulo, a proposed common backend proof format for heterogeneous proof assistants.</description>
<date>2012-06-30</date>
</dc>
</metadata>
</record>
</GetRecord>
</OAI-PMH>
