A comprehensible guide to a new unifier for CIC including universe polymorphism and overloading
| Autor: | Beta Ziliani, Matthieu Sozeau |
|---|---|
| Přispěvatelé: | Max Planck Institute for Software Systems (MPI-SWS), Design, study and implementation of languages for proofs and programs ( PI.R2 ), Preuves, Programmes et Systèmes (PPS), Centre National de la Recherche Scientifique (CNRS)-Université Paris Diderot - Paris 7 (UPD7)-Centre National de la Recherche Scientifique (CNRS)-Université Paris Diderot - Paris 7 (UPD7)-Inria Paris-Rocquencourt, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Université Paris Diderot - Paris 7 (UPD7)-Centre National de la Recherche Scientifique (CNRS)-Université Paris Diderot - Paris 7 (UPD7)-Centre National de la Recherche Scientifique (CNRS)-Inria Paris-Rocquencourt |
| Rok vydání: | 2017 |
| Předmět: |
Theoretical computer science
Unification Computer science CALCULUS OF INDUCTIVE CONSTRUCTIONS 0102 computer and information sciences 02 engineering and technology 01 natural sciences UNIFICATION 0202 electrical engineering electronic engineering information engineering COQ [INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL] business.industry Core component Proof assistant 020207 software engineering Small set Ciencias de la Computación Undecidable problem TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES 010201 computation theory & mathematics Ciencias de la Computación e Información TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS Artificial intelligence business Heuristics CIENCIAS NATURALES Y EXACTAS Software |
| Zdroj: | Journal of Functional Programming Journal of Functional Programming, Cambridge University Press (CUP), 2017, 27, ⟨10.1017/S0956796817000028⟩ Journal of Functional Programming, 2017, 27, ⟨10.1017/S0956796817000028⟩ |
| ISSN: | 1469-7653 0956-7968 |
| DOI: | 10.1017/s0956796817000028 |
| Popis: | 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. 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 Fil: Sozeau, Matthieu. Université Paris Diderot - Paris 7; Francia |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|