Groupoïd la Infini

Le langage de l'espace

le modèle

Voici le modèle conceptuel d'un système de démonstration de théorèmes qui unifie les théories de types tour avec des composants d'exécution (en tant que cibles d'extraction). Le modèle comprend: 1) des calculs avec ses modèles; 2) programmes et bibliothèques de base; et 3) les transformations de programme: vérification de type, compilation, effacement de type, extraction de code, optimisation, etc.

Tout en étant un modèle générique, certaines parties du modèle sont implémentées dans différentes langues. La recherche a été fondée par le centre de recherche Synrc de Kiev, en Ukraine. Tous les travaux ont été réalisés sous la supervision de Pavlo Maslianko, faculté de mathématiques appliquées de l'Université technique nationale d'Ukraine.

TAXONOMIE

La thèse est regroupée par domaines de recherche avec leurs systèmes de types, modèles formels, vérificateurs de types et bibliothèques de base correspondants.

la genèse

Le processus de vérification formelle comporte les phases suivantes: 1) codage du modèle, 2) liaison avec la bibliothèque de base de composants mathématiques, 3) désinsertion de fonctions essentielles, 3) liaison avec la bibliothèque de base pure et 4) extraction.

Modèle minimal. Ce modèle peut servir à la recherche PTS (Pure Type System), en tant que système de calcul de construction (CdC) avec un nombre infini d'univers avec extraction de programmes purs sur un interprète certifié.



Modèle cubique. Ce modèle peut servir à la recherche HoTT, étant le système MLTT / CCHM (théorie de type de Martin-Löf, Cohen-Coquand-Huber-Mörtberg) avec extraction limitée des programmes purs à un interprète certifié.


Modèle spectral. Ce modèle est destiné aux besoins du serveur en matière de liaison avec les exécutions de π-calcul et, éventuellement, les calculs et les moteurs de fusion. Extraction vers un interpréteur Erlang ou CPS (style de continuation).


Fascicule de Résultats

Articles évalués par des pairs sur les fondements de la théorie des types d'homotopie et la formalisation des mathématiques, détails de mise en œuvre et exemples d'applications pratiques. Voir cubical.systems pour plus d'informations.

Issue I: Internalizing Martin-Löf Type Theory

Issue III: Homotopy Type Theory

Issue VIII: Formal Topos on Category of Sets

Addendum I: Pure Type System for Erlang

Addendum II: Many Faces of Equality

Pour les notes en cours, voir la page du cours.