Heterogeneous Substitution Systems Revisited
In: hal-02360681;; (2018)
Online
Buch
Zugriff:
International audience ; Matthes and Uustalu (TCS 327(1-2):155-174, 2004) presented a categorical description of substitution systems capable of capturing syntax involving binding which is independent of whether the syntax is made up from least or greatest fixed points. We extend this work in two directions: we continue the analysis by creating more categorical structure, in particular by organizing substitution systems into a category and studying its properties, and we develop the proofs of the results of the cited paper and our new ones in UniMath, a recent library of univalent mathematics formalized in the Coq theorem prover.
| Titel: |
Heterogeneous Substitution Systems Revisited
|
|---|---|
| Autor/in / Beteiligte Person: | Ahrens, Benedikt ; Matthes, Ralph ; Gallinette : vers une nouvelle génération d'assistant à la preuve (LS2N - équipe 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) ; 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)-Université de Nantes - UFR des Sciences et des Techniques (UN UFR ST) ; Institut Mines-Télécom Paris (IMT)-Institut Mines-Télécom Paris (IMT) ; Assistance à la Certification d’Applications DIstribuées et Embarquées (IRIT-ACADIE) ; Institut de recherche en informatique de Toulouse (IRIT) ; Université Toulouse Capitole (UT Capitole) ; Université de Toulouse (UT)-Université de Toulouse (UT)-Université Toulouse - Jean Jaurès (UT2J) ; Université de Toulouse (UT)-Université Toulouse III - Paul Sabatier (UT3) ; Université de Toulouse (UT)-Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique (Toulouse) (Toulouse INP) ; Université de Toulouse (UT)-Toulouse Mind & Brain Institut (TMBI) ; Université Toulouse - Jean Jaurès (UT2J) ; Université de Toulouse (UT)-Université de Toulouse (UT)-Université Toulouse III - Paul Sabatier (UT3) ; Université de Toulouse (UT)-Université Toulouse Capitole (UT Capitole) ; Université de Toulouse (UT) ; Centre National de la Recherche Scientifique (CNRS) ; Uustalu, Tarmo ; ANR-11-IDEX-0002,UNITI,Université Fédérale de Toulouse(2011) ; ANR-11-LABX-0040,CIMI,Centre International de Mathématiques et d'Informatique (de Toulouse)(2011) ; European Project: 637339,H2020 ERC,ERC-2014-STG,CoqHoTT(2015) |
| Link: | |
| Quelle: | hal-02360681;; (2018) |
| Veröffentlichung: | HAL CCSD ; Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2018 |
| Medientyp: | Buch |
| ISBN: | 978-3-95977-030-9 (print) ; 3-95977-030-8 (print) |
| DOI: | 10.4230/LIPIcs.TYPES.2015.2 |
| Schlagwort: |
|
| Sonstiges: |
|