Effective metatheory for type theory : PhD thesis

Haselwarter, Philipp Georg (avtor), Bauer, Andrej (mentor)

In this dissertation, I propose finitary type theories as a definition of a wide class of type theories in the style of Martin-Löf, and I design a programming language for deriving judgements in finitary type theories. State of the art computer implementations of type theory rely on a computational interpretation of type theory, either via decidability results or via realisability. Such results are not readily available for all type theories studied in the literature, which renders their implementation challenging. The implementation of a flexible proof assistant supporting user-specified type theories requires a general definition outlining the structure of a type theory. I give a mathematically precise definition of a class of finitary type theories, that covers familiar examples, including Extensional Type Theory, the Calculus of Constructions, and Homotopy Type Theory. I first focus on the mathematical development of finitary type theories, before turning to their implementation in proof assistants. The definition proceeds in stages, starting with raw syntax, raw rules, and raw type theories, then delineating finitary rules and type theories, and finally specifying standard type theories. Once these definitions are accomplished, general meta-theoretic results in the form of a uniqueness of typing theorem and a cut elimination theorem are proved. I reformulate finitary type theories with a suitable treatment of free variables as context-free type theories, paving the way to an implementation in a proof assistant. The definition of context-free type theories again proceeds in stages of refinement, and I prove metatheorems for each successive stage. Translation theorems between context-free and finitary type theories relate the two formalisms. I introduce the Andromeda metalanguage (AML), an effectful programming language that allows convenient manipulation of judgement and rules of user-definable context-free type theories, and supports common proof development techniques. AML leverages algebraic effects and runners to extend proof assistant algorithms with local hypothesis in a modular way. The operational semantics of AML is inspired by bidirectional typing and helps the user harness contextual information, exhibiting a virtuous interaction with effect operations. AML has been implemented in the Andromeda prover, and I describe first experiments in the computer-assisted development of context-free type theories in AML.

• Jezik: Angleški jezik
• Ključne besede: dependent type theory, algebraic theory, proof assistant, metalanguage, computational effects
• Vrsta gradiva: Doktorsko delo/naloga
• Organizacija: FMF - Fakulteta za matematiko in fiziko
• Leto izida: 2022
• PID: 20.500.12556/RUL-134439
• UDK: 510.6
• COBISS.SI-ID: 94707203
• Datum objave v RUL: 14.01.2022

Sekundarni jezik

• Jezik: Slovenski jezik
• Naslov: Učinkovalna meta-teorija za teorijo tipov

Izvleček

V disertaciji definiram končne teorije tipov kot širok razred teorij tipov v stilu Martina-Löfa in oblikujem programski jezik za izpeljevanje sodb v splošnih teorijah tipov. Sodobne računalniške implementacije teorije tipov se zanašajo na njeno računsko interpretacijo bodisi preko rezultatov o odločljivosti ali realizabilnosti. Takšni rezultati pa niso na voljo za vse teorije tipov, ki jih srečamo v literaturi, zato njihova implementacija predstavlja izziv. Radi bi implementirali fleksibilen dokazovalni pomočnik, ki omogoča, da uporabnik sam določi teorijo tipov. Za to pa potrebujemo splošno definicijo teorije tipov, ki oriše njeno strukturo. V disertaciji podam matematično natančno definicijo razreda končnih teorij tipov, ki pokrije znane primere, vključno z ekstenzionalno teorijo tipov, računom konstrukcij in homotopsko teorijo tipov. Najprej se osredotočim na matematični razvoj končnih teorij tipov, preden se posvetim njihovi implementaciji v dokazovalnih pomočnikih. Definicija je zgrajena po stopnjah. Začnemo s surovo sintakso, surovimi pravili in surovimi teorijami tipov, nato razmejimo končna pravila in teorije tipov ter na koncu opredelimo standardne teorije tipov. S temi definicijami lahko dokažemo tudi metateoretične rezultate kot sta izrek o enoličnosti tipov in izrek o eliminaciji rezov. Da bi končne teorije tipov lažje implementirali v dokazovalnem pomočniku, jih preoblikujem v kontekstno neodvisne teorije tipov, ki omogočajo pravilno ravnanje s prostimi spremenljivkami. Definicija kontekstno neodvisnih teorij tipov je ponovno zgrajena po stopnjah. Za vsako stopnjo dokažem primerne metaizreke. Formalizma končnih torij tipov in kontekstno neodvisnih teorij tipov sta povezana preko izrekov prevedbe. Uvedem metajezik Andromeda (AML), učinkovni programski jezik, ki omogoča priročno ravnanje s sodbami in pravili v kontekstno neodvisnih teorijah tipov, ki jih uporabnik lahko sam določi. Jezik tudi podpira običajne tehnike za razvoj dokazov. AML izkoristi algebrajske učinke in poganjalce, da na modularen način z lokalnimi hipotezami razširi algoritme v dokazovalnih pomočnikih. Operacijska semantika jezika AML se naslanja na dvosmerno tipiziranje in pomaga uporabniku unovčiti informacije o kontekstu. S tem pokaže uspešno interakcijo z operacijami učinkov. AML je implementiran v dokazovalnem pomočniku Andromeda. Opišem tudi prve poskuse razvoja kontekstno neodvisnih teorij tipov z računalniško pomočjo v AML.

• Ključne besede: odvisna teorija tipov, algebrajska teorija, dokazovalni pomočnik, metajezik, računski učinki