Implementation of the Veritas Design Logic
Keith J. Hanna, Neil Daeche, Gareth Howells · 1992
Veritas is a design logic that provides dependent types and subtypes. It is implemented within the functional programming language Haskell. Interesting aspects of this implementation, in particular those relating to dependent types, to the representation of terms and signatures, to syntactic variants (controlled by attributes) and to a concrete notation for derivations are discussed.