Dependent Types and Formal Synthesis

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 available from this repository)

The full text of this publication is not available from this repository. (Contact us about this Publication)
Official URL
http://dx.doi.org/10.1098/rsta.1992.0029

Abstract

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.

Item Type: Article
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: http://kar.kent.ac.uk/id/eprint/22604 (The current URI for this page, for reference purposes)
  • Depositors only (login required):