Jan Christian Menz: Bachelor's Thesis

Programming Systems

Jan Christian Menz

Bachelor's Thesis

A Coq Library for Finite Types

Advisor: Gert Smolka

Abstract:

For my For my Bachelor's thesis I developed a library for finite types in the proof assistant Coq. This includes the definition of basic finite types, features like decidability, cardinality, a constructive choice function, and type operations like option, (dependent) pairing, sum, taking subtypes and the conversion from lists to finite types. The library defines vectors as a way to represent extensional functions with a finite domain and implements an iterative algorithm to obtain subsets of finite types.

Canonical structures, coercions and type classes are used to minimize the notational burden for the user. The library is tested with a small formalisation of finite automata including closure and decidability properties and the conversion between deterministic and nondeterministic automata.

The pre-existing Ssreflect library for finite types serves as an orientation. The goal is to achieve a compact and understandable development in pure Coq.

References

• Canonical Structures for the working Coq user (2013)
  Mahboubi, Assia and Tassi, Enrico
• Ssreflect
  Tassi, Enrico and Gonthier, Georges et. al
• A Gentle Introduction to Type Classes and Relations in Coq (2014)
  Casteran, Pierre and Sozeau,Matthieu
  
• Introduction to Computational Logic Lecture Notes SS 2014 (2014)
  Smolka, Gert and Brown, Chad E.
  
• Base library for ICL (2016)
  Smolka, Gert
• A Modular Formalisation of Finite Group Theory (2007)
  Georges Gonthier, Assia Mahboubi, Laurence Rideau, Enrico Tassi, Laurent Thery
  
• Hereditarily Finite Sets in Constructive Type Theory (2016)
  Smolka, Gert and Stark, Kathrin
  
• Generic Proof Tools and Finite Group Theory (2011)
  Francois Garillot
  
• A Constructive Theory of Regular Languages in Coq (2013)
  Christian Doczkal, Jan-Oliver Kaiser, and Gert Smolka
  
• Two-Way Automata in Coq (2016)
  Christian Doczkal, and Gert Smolka
  
• Duality principle (retrieved July 2016)
  Encyclopedia of Mathematics
  
• Dependently Typed Programming with Finite Sets (2015)
  Firsov, Denis and Uustalu, Tarmo
  
• Packaging Mathematical Structures (2009)
  Francois Garillot and Georges Gonthier and Assia Mahboubi and Laurence Rideau
  
• A Small Scale Reflection Extension for the Coq system (2015)
  Georges Gonthier , Assia Mahboubi and Enrico Tassi
  
• A Coherence Theorem for Martin-Loef's Type Theory (1998)
  Georges Gonthier , Assia Mahboubi and Enrico Tassi
  
• Automata and Computability (1997)
  Dexter C. Kozen
  
• Introduction to Computational Logic. Lecture Notes (2014)
  Gert Smolka and Chad E. Brown
  
• Type Classes for Mathematics in Type Theory (2011)
  Bas Spitters and Eelis van der Weegen
  
• The Coq Proof Assistant The standard library (version 2016)
  The Coq development team