Hanna, Keith and Daeche, N. and Howells, G. (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 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:||20 May 2011 23:30|
|Resource URI:||http://kar.kent.ac.uk/id/eprint/22608 (The current URI for this page, for reference purposes)|
- Depositors only (login required):