HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation

A Logical Framework to Prove Properties of Alpha Programs

Luc Bougé 1 David Cachera 1
1 REMAP - Regularity and massive parallel computing
Inria Grenoble - Rhône-Alpes, LIP - Laboratoire de l'Informatique du Parallélisme
Abstract : We present an assertional approach to prove properties of Alpha programs. Alpha is a functional language based on affine recurrence equations. We first present two kinds of operational semantics for Alpha together with some equivalence andconfluence properties of these semantics. We then present an attempt to provide Alpha with an external logical framework. We therefore define a proof method based on invariants. We focus on a particular class of invariants, namely canonical invariants, that are a logical expression of the program's semantics. We finally show that this framework is well-suited to prove equivalence properties between Alpha programs.
Document type :
Complete list of metadata

Contributor : Rapport de Recherche Inria Connect in order to contact the contributor
Submitted on : Wednesday, May 24, 2006 - 1:26:27 PM
Last modification on : Friday, February 4, 2022 - 3:19:19 AM
Long-term archiving on: : Sunday, April 4, 2010 - 11:53:57 PM


  • HAL Id : inria-00073662, version 1



Luc Bougé, David Cachera. A Logical Framework to Prove Properties of Alpha Programs. [Research Report] RR-3031, INRIA. 1996. ⟨inria-00073662⟩



Record views


Files downloads