Please use this identifier to cite or link to this item: doi:10.22028/D291-30298
Title: Mechanising syntax with binders in Coq
Author(s): Stark, Kathrin
Language: English
Year of Publication: 2019
DDC notations: 004 Computer science, internet
Publikation type: Doctoral Thesis
Abstract: Mechanising binders in general-purpose proof assistants such as Coq is cumbersome and difficult. Yet binders, substitutions, and instantiation of terms with substitutions are a critical ingredient of many programming languages. Any practicable mechanisation of the meta-theory of the latter hence requires a lean formalisation of the former. We investigate the topic from three angles: First, we realise formal systems with binders based on both pure and scoped de Bruijn algebras together with basic syntactic rewriting lemmas and automation. We automate this process in a compiler called Autosubst; our final tool supports many-sorted, variadic, and modular syntax. Second, we justify our choice of realisation and mechanise a proof of convergence of the sigma calculus, a calculus of explicit substitutions that is complete for equality of the de Bruijn algebra corresponding to the lambda calculus. Third, to demonstrate the practical usefulness of our approach, we provide concise, transparent, and accessible mechanised proofs for a variety of case studies refined to de Bruijn substitutions.
Die Mechanisierung von Bindern in universellen Beweisassistenten wie Coq ist arbeitsaufwändig und schwierig. Binder, Substitutionen und die Instantiierung von Substitutionen sind jedoch kritischer Bestandteil vieler Programmiersprachen. Deshalb setzt eine praktikable Mechanisierung der Metatheorie von Programmiersprachen eine elegante Formalisierung von Bindern voraus. Wir nähern uns dem Thema aus drei Richtungen an: Zuerst realisieren wir formale Systeme mit Bindern mit Hilfe von reinen und indizierten de Bruijn Algebren, zusammen mit grundlegenden syntaktischen Gleichungen und Automatisierung. Wir automatisieren diesen Prozess in einem Kompilierer namens Autosubst. Unser finaler Kompilierer unterstützt Sortenlogik, variadische Syntax und modulare Syntax. Zweitens rechtfertigen wir unsere Repräsentation und mechanisieren einen Beweis der Konvergenz des SP-Kalküls, einem Kalkül expliziter Substitutionen der bezüglich der Gleichheit der puren de Bruijn Algebra des -Kalküls vollständig ist. Drittens entwickeln wir kurze, transparente und leicht zugängliche mechanisierte Beweise für diverse Fallstudien, die wir an de Bruijn Substitutionen angepasst haben. Wir weisen so die praktische Anwendbarkeit unseres Ansatzes nach.
Link to this record: urn:nbn:de:bsz:291--ds-302986
hdl:20.500.11880/28822
http://dx.doi.org/10.22028/D291-30298
Advisor: Smolka, Gert
Date of oral examination: 14-Feb-2020
Date of registration: 3-Mar-2020
Faculty: MI - Fakultät für Mathematik und Informatik
Department: MI - Informatik
Professorship: MI - Prof. Dr. Gert Smolka
Collections:SciDok - Der Wissenschaftsserver der Universität des Saarlandes

Files for this record:
File Description SizeFormat 
thesis (1).pdfThesis1,22 MBAdobe PDFView/Open


Items in SciDok are protected by copyright, with all rights reserved, unless otherwise indicated.