Implementation of the Veritas Design Logic

Hanna, Keith and Daeche, Neil and Howells, Gareth (1992) Implementation of the Veritas Design Logic. In: International Conference On Theorem Provers in Circuit Design : Theory, Practice And Experience. IFIP Transactions A-Computer Science and Technology , 10. Elsevier Science BV , Nijmegen, Netherlands pp. 77-94. ISBN 0-444-89686-4. (The full text of this publication is not currently available from this repository. You may be able to access a copy if URLs are provided)

The full text of this publication is not available from this repository. (Contact us about this Publication)


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.

Item Type: Conference or workshop item (Paper)
Uncontrolled keywords: Design Logic; Dependent Types; Implementation
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 75 Electronic computers. Computer science
Divisions: Faculties > Science Technology and Medical Studies > School of Computing
Depositing User: P. Ogbuji
Date Deposited: 08 Sep 2009 08:38
Last Modified: 28 Apr 2014 09:25
Resource URI: (The current URI for this page, for reference purposes)
  • Depositors only (login required):