Jan Christian Menz: Bachelor's Thesis

Saarland University Computer Science

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

Thesis

Coq development

Presentations

  • Initial Seminar Talk: Slides (May 13, 2016)
  • Second Seminar Talk: Slides (June 17, 2016)
  • Final Talk: Slides (July 29, 2016)


Jan Christian Menz, Tue Dec 6 18:42:26 2016