Gilles Nies: Bachelor Thesis

Saarland University Computer Science

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.




The finished thesis can be downloaded here.

Coq developments

Legal notice, Privacy policy