Hanna, F.K. and Daeche, N. (1992) Dependent Types and Formal Synthesis. Philosophical Transactions of the Royal Society of London Series a-Mathematical Physical and Engineering Sciences, 339 (1652). pp. 121-135. ISSN 0962-8428.
|The full text of this publication is not available from this repository. (Contact us about this Publication)|
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:||13 Jun 2012 09:33|
|Resource URI:||http://kar.kent.ac.uk/id/eprint/22604 (The current URI for this page, for reference purposes)|
- Depositors only (login required):