Pragmatic isomorphism proofs between coq representations: application to lambda-term families
In: TYPES 2022 : 28th International Conference on Types for Proofs and Programs ; 28th International Conference on Types for Proofs and Programs (TYPES 2022) ; https://hal.science/hal-04245455 ; 28th International Conference on Types for Proofs and Programs (TYPES 2022), Jun 2022, Nantes, France. pp.11:1-11:19, ⟨10.4230/LIPIcs.TYPES.2022.11⟩, 2022
Online
Konferenz
Zugriff:
| Titel: |
Pragmatic isomorphism proofs between coq representations: application to lambda-term families
|
|---|---|
| Autor/in / Beteiligte Person: | Dubois, Catherine ; Magaud, Nicolas ; Giorgetti, Alain ; Institut Polytechnique de Paris (IP Paris) ; Architecture, Cloud continuum, formal Models, artificial intElligence and Services in distributed computing (ACMES-SAMOVAR) ; Services répartis, Architectures, MOdélisation, Validation, Administration des Réseaux (SAMOVAR) ; Institut Mines-Télécom Paris (IMT)-Télécom SudParis (TSP)-Institut Mines-Télécom Paris (IMT)-Télécom SudParis (TSP) ; Laboratoire des sciences de l'ingénieur, de l'informatique et de l'imagerie (ICube) ; École Nationale du Génie de l'Eau et de l'Environnement de Strasbourg (ENGEES)-Université de Strasbourg (UNISTRA)-Institut National des Sciences Appliquées - Strasbourg (INSA Strasbourg) ; Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Les Hôpitaux Universitaires de Strasbourg (HUS)-Centre National de la Recherche Scientifique (CNRS)-Matériaux et Nanosciences Grand-Est (MNGE) ; Université de Strasbourg (UNISTRA)-Université de Haute-Alsace (UHA) Mulhouse - Colmar (Université de Haute-Alsace (UHA))-Institut National de la Santé et de la Recherche Médicale (INSERM)-Institut de Chimie - CNRS Chimie (INC-CNRS)-Centre National de la Recherche Scientifique (CNRS)-Université de Strasbourg (UNISTRA)-Université de Haute-Alsace (UHA) Mulhouse - Colmar (Université de Haute-Alsace (UHA))-Institut National de la Santé et de la Recherche Médicale (INSERM)-Institut de Chimie - CNRS Chimie (INC-CNRS)-Centre National de la Recherche Scientifique (CNRS)-Réseau nanophotonique et optique ; Université de Strasbourg (UNISTRA)-Université de Haute-Alsace (UHA) Mulhouse - Colmar (Université de Haute-Alsace (UHA))-Centre National de la Recherche Scientifique (CNRS)-Université de Strasbourg (UNISTRA)-Centre National de la Recherche Scientifique (CNRS) ; Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies (UMR 6174) (FEMTO-ST) ; Université de Technologie de Belfort-Montbeliard (UTBM)-Ecole Nationale Supérieure de Mécanique et des Microtechniques (ENSMM)-Centre National de la Recherche Scientifique (CNRS)-Université de Franche-Comté (UFC) ; Université Bourgogne Franche-Comté COMUE (UBFC)-Université Bourgogne Franche-Comté COMUE (UBFC) ; ANR-17-EURE-0002,EIPHI,Ingénierie et Innovation par les sciences physiques, les savoir-faire technologiques et l'interdisciplinarité(2017) ; ANR-11-LABX-0055,IRMIA,Institut de Recherche en Mathématiques, ses Interactions et Applications(2011) |
| Link: | |
| Zeitschrift: | TYPES 2022 : 28th International Conference on Types for Proofs and Programs ; 28th International Conference on Types for Proofs and Programs (TYPES 2022) ; https://hal.science/hal-04245455 ; 28th International Conference on Types for Proofs and Programs (TYPES 2022), Jun 2022, Nantes, France. pp.11:1-11:19, ⟨10.4230/LIPIcs.TYPES.2022.11⟩, 2022 |
| Veröffentlichung: | HAL CCSD, 2022 |
| Medientyp: | Konferenz |
| DOI: | 10.4230/LIPIcs.TYPES.2022.11 |
| Schlagwort: |
|
| Sonstiges: |
|