Mostrar el registro sencillo del ítem
dc.contributor.author
Ziliani, Luis Francisco
![Se ha confirmado la validez de este valor de autoridad por un usuario](/themes/CONICETDigital/images/authority_control/invisible.gif)
dc.contributor.author
Sozeau, Matthieu
dc.date.available
2019-03-25T20:00:55Z
dc.date.issued
2017-02
dc.identifier.citation
Ziliani, Luis Francisco; Sozeau, Matthieu; A comprehensible guide to a new unifier for CIC including universe polymorphism and overloading; Cambridge University Press; Journal Of Functional Programming; 27; 2-2017; 1-58
dc.identifier.issn
0956-7968
dc.identifier.uri
http://hdl.handle.net/11336/72454
dc.description.abstract
Unification is a core component of every proof assistant or programming language featuring dependent types. In many cases, it must deal with higher order problems up to conversion. Since unification in such conditions is undecidable, unification algorithms may include several heuristics to solve common problems. However, when the stack of heuristics grows large, the result and complexity of the algorithm can become unpredictable. Our contributions are twofold: (1) We present a full description of a new unification algorithm for the Calculus of Inductive Constructions (the base logic of COQ), building it up from a basic calculus to the full Calculus of Inductive Constructions as it is implemented in COQ, including universe polymorphism, canonical structures (the overloading mechanism baked into COQ's unification), and a small set of useful heuristics. (2) We implemented our algorithm, and tested it on several libraries, providing evidence that the selected set of heuristics suffices for large developments.
dc.format
application/pdf
dc.language.iso
eng
dc.publisher
Cambridge University Press
![Se ha confirmado la validez de este valor de autoridad por un usuario](/themes/CONICETDigital/images/authority_control/invisible.gif)
dc.rights
info:eu-repo/semantics/openAccess
dc.rights.uri
https://creativecommons.org/licenses/by-nc-sa/2.5/ar/
dc.subject
Unification
dc.subject
Calculus of Inductive Constructions
dc.subject
Coq
dc.subject.classification
Ciencias de la Computación
![Se ha confirmado la validez de este valor de autoridad por un usuario](/themes/CONICETDigital/images/authority_control/invisible.gif)
dc.subject.classification
Ciencias de la Computación e Información
![Se ha confirmado la validez de este valor de autoridad por un usuario](/themes/CONICETDigital/images/authority_control/invisible.gif)
dc.subject.classification
CIENCIAS NATURALES Y EXACTAS
![Se ha confirmado la validez de este valor de autoridad por un usuario](/themes/CONICETDigital/images/authority_control/invisible.gif)
dc.title
A comprehensible guide to a new unifier for CIC including universe polymorphism and overloading
dc.type
info:eu-repo/semantics/article
dc.type
info:ar-repo/semantics/artículo
dc.type
info:eu-repo/semantics/publishedVersion
dc.date.updated
2019-03-21T14:09:45Z
dc.journal.volume
27
dc.journal.pagination
1-58
dc.journal.pais
Reino Unido
![Se ha confirmado la validez de este valor de autoridad por un usuario](/themes/CONICETDigital/images/authority_control/invisible.gif)
dc.journal.ciudad
Cambridge
dc.description.fil
Fil: Ziliani, Luis Francisco. Universidad Nacional de Córdoba. Facultad de Matemática, Astronomía y Física; Argentina. Consejo Nacional de Investigaciones Científicas y Técnicas; Argentina
dc.description.fil
Fil: Sozeau, Matthieu. Université Paris Diderot - Paris 7; Francia
dc.journal.title
Journal Of Functional Programming
![Se ha confirmado la validez de este valor de autoridad por un usuario](/themes/CONICETDigital/images/authority_control/invisible.gif)
dc.relation.alternativeid
info:eu-repo/semantics/altIdentifier/doi/http://dx.doi.org/10.1017/S0956796817000028
dc.relation.alternativeid
info:eu-repo/semantics/altIdentifier/url/https://www.cambridge.org/core/journals/journal-of-functional-programming/article/comprehensible-guide-to-a-new-unifier-for-cic-including-universe-polymorphism-and-overloading/19A095CA0645F89A772B7E2B7B3D92B2
Archivos asociados