Encoding Agda Programs Using Rewriting
| Autor: | Genestier, Guillaume |
|---|---|
| Přispěvatelé: | Laboratoire Spécification et Vérification (LSV), Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), Université Paris-Saclay, Centre National de la Recherche Scientifique (CNRS), Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), Deduction modulo, interopérabilité et démonstration automatique (DEDUCTEAM), Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Spécification et Vérification (LSV), Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), Mines Paris - PSL (École nationale supérieure des mines de Paris), Université Paris sciences et lettres (PSL) |
| Jazyk: | angličtina |
| Rok vydání: | 2020 |
| Předmět: |
Logical Frameworks
Rewriting [MATH.MATH-LO]Mathematics [math]/Logic [math.LO] [INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL] Eta Conversion Universe Polymorphism Theory of computation → Equational logic and rewriting [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO] Theory of computation → Type theory |
| Zdroj: | FSCD-5th International Conference on Formal Structures for Computation and Deduction FSCD-5th International Conference on Formal Structures for Computation and Deduction, Jun 2020, Paris, France. ⟨10.4230/LIPIcs.FSCD.2020.31⟩ |
| DOI: | 10.4230/LIPIcs.FSCD.2020.31⟩ |
| Popis: | International audience; We present in this paper an encoding in an extension with rewriting of the Edimburgh Logical Framework (LF) [Harper et al., 1993] of two common features: universe polymorphism and eta-convertibility. This encoding is at the root of the translator between Agda and Dedukti developped by the author. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|