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 preexisting 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, JanOliver Kaiser, and Gert Smolka

TwoWay 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 MartinLoef'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
Thesis
Coq development
Presentations

Initial Seminar Talk: Slides (May 13, 2016)

Second Seminar Talk: Slides (June 17, 2016)

Final Talk: Slides (July 29, 2016)
Legal notice, Privacy policy