Proving a real time algorithm for ATM in Coq
In: Types for proofs and programs (Aussois, 15-19 December 1996, selected papers)Lecture notes in computer science; (1998) S. 277-293
Konferenz
- print, 9 ref
Zugriff:
This paper presents the techniques used for proving, in the framework of type theory, the correctness of an algorithm recently standardized at ITU-T that handles time explicitly. The structure of the proof and its formalization in Coq are described, as well as the main tools which have been developed: an abstract model of real-time that makes no assumption on the nature of time and a way to actually find proofs employing transitivity, using only logical definitions and an existing tactic.
Titel: |
Proving a real time algorithm for ATM in Coq
|
---|---|
Autor/in / Beteiligte Person: | MONIN, J.-F |
Link: | |
Quelle: | Types for proofs and programs (Aussois, 15-19 December 1996, selected papers)Lecture notes in computer science; (1998) S. 277-293 |
Veröffentlichung: | Berlin; New York NY: Springer-Verlag, 1998 |
Medientyp: | Konferenz |
Umfang: | print, 9 ref |
ISSN: | 0302-9743 (print) |
Schlagwort: |
|
Sonstiges: |
|