index.pug

extends layout.pug

block title
    script(src='//cdnjs.cloudflare.com/ajax/libs/mathjax/2.6.0/MathJax.js?config=TeX-AMS-MML_HTMLorMML')
    script.
       MathJax.Hub.Config({
          tex2jax: { inlineMath: [['$','$'], ['\\(','\\)']], processEscapes: true },
          jax: ["input/TeX", "input/MathML", "input/AsciiMath", "output/CommonHTML", "output/NativeMML"],
          TeX: { extensions: ["AMSmath.js", "AMSsymbols.js", "autoload-all.js"] },
          extensions: ["tex2jax.js", "asciimath2jax.js", "mml2jax.js", "MathMenu.js", "MathZoom.js"],
          "HTML-CSS": { imageFont: null },
       });
    title Infinity

block content
    +header('groupoid.svg', 'Groupoïd la Infini', 'Le langage de l\'espace')
    article.main
        .om
            section
                h1 le modèle

            aside <a href="https://tonpa.guru">Максим Сохацький</a>
                time 20 DEC 2018
            p.
                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.
            p.
                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.

            section
                h1 TAXONOMIE
            p.
                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.

        .index
            .index__col
                h2 CPS
                ul
                    li: a(href='lambda/intro') Verified Interpreter
                    li: a(href='lambda/extract') Extraction
            .index__col
                h2 PTS/MLTT/CiC
                ul
                    li: a(href='#pts/intro') Intro
                    li: a(href='pts/pure') Pure Core
                    li: a(href='mltt/inductive') Inductive Core
                    li: a(href='pts/semantics') Semantics
            .index__col
                h2 EFFECTS
                ul
                    li <a href='eff/io'>I/O</a>
                    li <a href='eff/ioi'>Infinity I/O</a>
                    li <a href='#eff/coq'>Coq Coeffects</a>
            .index__col
                h2 RUN-TIME
                ul
                    li: a(href='pi/intro') Intro
                    li: a(href='lambda/runtime') Runtime
                    li: a(href='#pi/check') Type Checking
                    li: a(href='#pi/bisim') Bisimulation
            .index__col
                h2 HoTT/CCHM
                ul
                    li: a(href='mltt/infinity') Language Overview
                    li: a(href='mltt/types') Math Components
                    li: a(href='course/') HoTT Course
                    li: a(href='mltt/hopf') IX. Hopf Fibrations
                    li: a(href='mltt/iso') B. Path Iso
                    li: a(href='mltt/topos') VIII. Set Topos
            .index__col
                h2 TENSOR STORE
                ul
                    li: a(href='/array/intro') Intro
                    li: a(href='#array/lang') The Language
                    li: a(href='#array/vec') Vectorization

        .om
            section
                h1 la genèse

            p.
                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.

            p.
                <b>Modèle minimal</b>. 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é.
            br.
            p.
                <object><center><img src="minimal.svg?v=6" width=50%></center></object>
            br.
            p.
                <b>Modèle cubique</b>. 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é.
            p.
                <object><center><img src="higher.svg?v=6" width=70%></center></object>
            br.
            p.
                <b>Modèle spectral</b>. 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).
            p.
                <object><center><img src="full.svg?v=6" width=90%></center></object>
            br.

            section
                h1 Fascicule de Résultats
            p.
                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 <a href="https://cubical.systems">cubical.systems</a>
                pour plus d'informations.

        .index

            <center><table cellspacing=5><tr><td width=5><img src="https://n2o.space/img/pdf.jpg" width=35></td><td width=400>
            <a href="https://github.com/groupoid/groupoid.space/blob/master/tex/articles/mltt/mltt.pdf">
            <h3>Issue I: Internalizing Martin-Löf Type Theory</h3>
            </a></td></tr></table></center>

            <center><table cellspacing=5><tr><td width=5><img src="https://n2o.space/img/pdf.jpg" width=35></td><td width=400>
            <a href="https://github.com/groupoid/groupoid.space/blob/master/tex/articles/hott/hott.pdf">
            <h3>Issue III: Homotopy Type Theory</h3>
            </a></td></tr></table></center>

            <center><table cellspacing=5><tr><td width=5><img src="https://n2o.space/img/pdf.jpg" width=35></td><td width=400>
            <a href="https://github.com/groupoid/groupoid.space/blob/master/tex/articles/topos/topos.pdf">
            <h3>Issue VIII: Formal Topos on Category of Sets</h3>
            </a></td></tr></table></center>

            <center><table cellspacing=5><tr><td width=5><img src="https://n2o.space/img/pdf.jpg" width=35></td><td width=400>
            <a href="https://github.com/groupoid/groupoid.space/blob/master/tex/articles/pts/pts.pdf">
            <h3>Addendum I: Pure Type System for Erlang</h3>
            </a></td></tr></table></center>

            <center><table cellspacing=5><tr><td width=5><img src="https://n2o.space/img/pdf.jpg" width=35></td><td width=400>
            <a href="https://github.com/groupoid/groupoid.space/blob/master/tex/articles/equ/equ.pdf">
            <h3>Addendum II: Many Faces of Equality</h3>
            </a></td></tr></table></center>

            p.
                Pour les notes en cours, voir <a href="/course/">la page du cours</a>.