Circuits as streams in COQ: verification of a sequential multiplier.

Abstract : This paper presents the proof of correctness of a multiplier circuit formalized in the calculus of inductive constructions. It uses a representation of the circuit as a function from the stream of inputs to the stream of outputs. We analyze the computational aspect of the impredicative encoding of coinductive types and show how it can be used to represent synchronous circuits. We identify general proof principles that can be used to justify the correctness of such a circuit. The example and the principles have been formalized in the Coq proof assistant.This paper presents the proof of correctness of a multiplier circuit formalized in the Calculus of Inductive Constructions. It uses a representation of the circuit as a function from the stream of inputs to the stream of outputs. We analyze the computational aspect of the impredicative encoding of coinductive types and show how it can be used to represent synchronous circuits. We identify general proof principles that can be used to justify the correctness of such a circuit. The example and the principles have been formalized in the Coq proof assistant.
Document type :
Reports
Complete list of metadatas

Cited literature [10 references]  Display  Hide  Download

https://hal-lara.archives-ouvertes.fr/hal-02101845
Contributor : Colette Orange <>
Submitted on : Wednesday, April 17, 2019 - 9:07:56 AM
Last modification on : Sunday, May 19, 2019 - 1:20:44 AM

File

RR1995-16.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-02101845, version 1

Collections

Citation

Christine Paulin-Mohring. Circuits as streams in COQ: verification of a sequential multiplier.. [Research Report] LIP RR-1995-16, Laboratoire de l'informatique du parallélisme. 1995, 2+15p. ⟨hal-02101845⟩

Share

Metrics

Record views

10

Files downloads

43