Circuits as streams in COQ: verification of a sequential multiplier. - Archive ouverte HAL Accéder directement au contenu
Rapport (Rapport De Recherche) Année : 1995

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

(1)
1

Résumé

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.
Cet article présente la preuve formalisée dans le calcul des constructions inductives de la correction d'un circuit réalisant la multiplication sur les entiers. Le circuit est représenté par une fonction transformant la suite infinie d'entrées en une suite infinie de sorties. Nous analysons l'aspect calculatoire de la représentation imprédicative des définitions co-inductives et montrons comment cette représentation peut servir à coder un circuit synchrone. Nous identifions des principes de preuve généraux pour justifier de tels circuits. Les exemples et les principes ont été formalisés dans l'assistant à la démonstration Coq.
Fichier principal
Vignette du fichier
RR1995-16.pdf (250.39 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-02101845 , version 1 (17-04-2019)

Identifiants

  • HAL Id : hal-02101845 , version 1

Citer

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⟩
13 Consultations
198 Téléchargements

Partager

Gmail Facebook Twitter LinkedIn More