Derivation of Static Analysers of Functional Programs from Path Properties of a Natural Semantics

Valérie Gouranton 1 Daniel Le Métayer 1
1 Lande - Logiciel : ANalyse et DEveloppement
IRISA - Institut de Recherche en Informatique et Systèmes Aléatoires, Inria Rennes – Bretagne Atlantique
Abstract : We advocate the use of operational semantics as a basis for specifying program analyses for functional languages. We put forward a methodology for defining a static analysis by successive refinements of the natural semantics of the language. We use paths as the abstract representation of proof trees and we provide a language for defining properties in terms of recurrence equations on paths. We show the specification of several standard properties on paths (neededness, absence, uniqueness, \ldots) and the mechanical derivation of the corresponding analyses
Document type :
Reports
Complete list of metadatas

https://hal.inria.fr/inria-00074078
Contributor : Rapport de Recherche Inria <>
Submitted on : Wednesday, May 24, 2006 - 2:26:55 PM
Last modification on : Thursday, November 29, 2018 - 6:18:06 PM
Long-term archiving on : Monday, April 5, 2010 - 12:04:36 AM

Identifiers

  • HAL Id : inria-00074078, version 1

Citation

Valérie Gouranton, Daniel Le Métayer. Derivation of Static Analysers of Functional Programs from Path Properties of a Natural Semantics. [Research Report] RR-2607, INRIA. 1995. ⟨inria-00074078⟩

Share

Metrics

Record views

185

Files downloads

142