Setoid type theory - a syntactic translation
| Autor: | Thorsten Altenkirch, Nicolas Tabareau, Simon Boulier, Ambrus Kaposi |
|---|---|
| Přispěvatelé: | Functional Programming Laboratory, University of Nottingham, UK (UON), Gallinette : vers une nouvelle génération d'assistant à la preuve (GALLINETTE), Inria Rennes – Bretagne Atlantique, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire des Sciences du Numérique de Nantes (LS2N), IMT Atlantique Bretagne-Pays de la Loire (IMT Atlantique), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT)-Université de Nantes - UFR des Sciences et des Techniques (UN UFR ST), Université de Nantes (UN)-Université de Nantes (UN)-École Centrale de Nantes (ECN)-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique Bretagne-Pays de la Loire (IMT Atlantique), Université de Nantes (UN)-Université de Nantes (UN)-École Centrale de Nantes (ECN)-Centre National de la Recherche Scientifique (CNRS), Laboratoire des Sciences du Numérique de Nantes (LS2N), Eötvös Loránd University (ELTE), Gallinette : vers une nouvelle génération d'assistant à la preuve (LS2N - équipe GALLINETTE), Université de Nantes - UFR des Sciences et des Techniques (UN UFR ST), Université de Nantes (UN)-Université de Nantes (UN)-École Centrale de Nantes (ECN)-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique (IMT Atlantique), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT) |
| Jazyk: | angličtina |
| Rok vydání: | 2019 |
| Předmět: |
050101 languages & linguistics
Conjecture [INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL] 05 social sciences 02 engineering and technology Function (mathematics) Type (model theory) 16. Peace & justice Syntax Algebra Type theory TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS Computer Science::Logic in Computer Science Extensionality 0202 electrical engineering electronic engineering information engineering Computer Science::Programming Languages 020201 artificial intelligence & image processing 0501 psychology and cognitive sciences Setoid Universe (mathematics) Mathematics |
| Zdroj: | MPC 2019-13th International Conference on Mathematics of Program Construction MPC 2019-13th International Conference on Mathematics of Program Construction, Oct 2019, Porto, Portugal. pp.155-196, ⟨10.1007/978-3-030-33636-3_7⟩ Lecture Notes in Computer Science ISBN: 9783030336356 MPC Mathematics of Program Construction-13th International Conference, MPC 2019, Porto, Portugal, October 7–9, 2019, Proceedings Lecture Notes in Computer Science Lecture Notes in Computer Science-Mathematics of Program Construction |
| ISSN: | 0302-9743 1611-3349 |
| DOI: | 10.1007/978-3-030-33636-3_7⟩ |
| Popis: | International audience; We introduce setoid type theory, an intensional type theory with a proof-irrelevant universe of propositions and an equality type satisfying function extensionality, propositional extensionality and a definitional computation rule for transport. We justify the rules of setoid type theory by a syntactic translation into a pure type theory with a universe of propositions. We conjecture that our syntax is complete with regards to this translation. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|