Hanna, Keith and Daeche, Neil (1992) Dependent Types and Formal Synthesis. Philosophical Transactions of the Royal Society A: Mathematical, Physical & Engineering Sciences., 339 (1652). pp. 121-135. ISSN 0261-0523. (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 relative advantages offered by the use of dependent types (rather than polymorphic ones) in a higher-order logic used for reasoning about digital systems are explored. Dependent types and subtypes are shown to provide an effective means of expressing the bounded. parametrized types typically encountered in this field. Heuristic methods can be used to minimize problems arising from the loss of decidable type-checking. A second topic discussed is formal synthesis, an approach to design in which the activities of behavioural synthesis and of formal verification are combined. The starting point is a behavioural specification. the end result is a specification of an implementation together with a proof of its correctness.
|Subjects:||Q Science > Q Science (General)|
|Divisions:||Faculties > Science Technology and Medical Studies > Centre for Music Technology|
|Depositing User:||P. Ogbuji|
|Date Deposited:||01 Oct 2009 08:08|
|Last Modified:||17 Jun 2014 15:24|
|Resource URI:||https://kar.kent.ac.uk/id/eprint/22604 (The current URI for this page, for reference purposes)|