Gilles Nies: Bachelor Thesis
Representations of Boolean functions in Constructive Type Theory
Author: Gilles Nies
Advisor: Chad E. Brown
Supervisor: Gert Smolka
Boolean functions are an abstraction of one of the most important computer hardware topics: circuits. They can be represented in many different ways like truth tables or logical expressions. While truth tables are often rejected because of their expensiveness in space, logical expressions come with an infinite number of representations for the same Boolean function. We give several definitions of Boolean functions, Decision Trees and Prime Trees in Coq and prove that Prime Trees give a canonical representation of Boolean functions. Sometimes this requires the assumption of consistent, yet unprovable propositions to circumvent some well-known problems in Coq.
27.09.2011, 15:15: First talk (Building E1 3, Room 528)
04.11.2011, 14:15: Proposal talk (Building E1 3, Room 528)
20.04.2012, 14:15: Final talk (Building E1 3, Room 528) slides
The finished thesis can be downloaded here.