Reasoning about array structures using a dependently typed logic

Dent, Alan and Hanna, Keith (1993) Reasoning about array structures using a dependently typed logic. In: Agnew, David and Claesen, Luc J. M. and Camposano, Raul, eds. IFIP transactions a-computer science and technology. Elsevier Science Publ B V pp. 207-224. ISBN 0-444-81641-0. (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)


This paper explores the use of a dependently-typed design logic for describing and reasoning about systolic arrays. Taking triangular arrays as an example, it is shown how they may usefully be defined in various equivalent ways and how their behaviour may be related to that of the corresponding one-dimensional systolic arrays. This allows complex proofs of the properties of such (dynamic) arrays to be replaced with simpler proofs of the properties of (static) dependency graphs. As an example, the correctness of a systolic sorter is formally established. Overall its is shown that the use of dependent types for describing systolic arrays contributes significantly to the clarity and generality of their specifications.

Item Type: Conference or workshop item (Paper)
Additional information: IFIP WG10.2 International Conference on Computer Hardware Description Languages and their Applications (CHDL 93) OTTAWA, CANADA, APR 26-28, 1993 INT FEDERAT INFORMAT PROC, WORKING GRP 10.2; IEEE, COMPSOC
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: R.F. Xu
Date Deposited: 15 Jul 2009 10:07
Last Modified: 13 Jun 2014 08:13
Resource URI: (The current URI for this page, for reference purposes)
  • Depositors only (login required):


Downloads per month over past year