scholarly journals A Framework for Formalization and Strictness Analysis of Simulation Event Orderings

SIMULATION ◽  
2005 ◽  
Vol 81 (4) ◽  
pp. 325-335 ◽  
Author(s):  
Y. M. Teo ◽  
B. S. S. Onggo
Keyword(s):  
Strictness Analysis

Proving the correctness of compiler optimisations based on a global analysis: a study of strictness analysis†

1996 ◽  
Vol 6 (1) ◽  
pp. 75-109 ◽  
Author(s):  
Geoffrey Burn ◽  
Daniel Le Métayer
Keyword(s):  
Global Analysis ◽  
Functional Languages ◽  
Correctness Proof ◽  
Formal Presentation ◽  
Strictness Analysis ◽  
Proof Of Correctness

AbstractA substantial amount of work has been devoted to the proof of correctness of various program analyses but much less attention has been paid to the correctness of compiler optimisations based on these analyses. In this paper we tackle the problem in the context of strictness analysis for lazy functional languages. We show that compiler optimisations based on strictness analysis can be expressed formally in the functional framework using continuations. This formal presentation has two benefits: it allows us to give a rigorous correctness proof of the optimised compiler; and it exposes the various optimisations made possible by a strictness analysis.

scholarly journals Bounded Fixed Point Iteration

1991 ◽  
Vol 20 (359) ◽  
Author(s):  
Hanne Riis Nielson ◽  
Flemming Nielson
Keyword(s):  
Fixed Point ◽  
Abstract Interpretation ◽  
Higher Order ◽  
Monotone Functions ◽  
Additive Functions ◽  
Fixed Point Iteration ◽  
Exponential Bound ◽  
Strictness Analysis ◽  
Long Chains

In the context of abstract interpretation for languages without higher-order features we study the number of times a functional need to be unfolded in order to give the least fixed point. For the cases of total or monotone functions we obtain an exponential bound and in the case of strict and additive (or distributive) functions we obtain a quadratic bound. These bounds are shown to be tight in that sufficiently long chains of functions can be shown to exist. Specializing the case of strict and additive functions to functionals of a form that would correspond to iterative programs we show that a linear bound is tight. This is related to several analyses studied in the literature (including strictness analysis).

Sign in / Sign up

Export Citation Format

Share Document