## User login## Navigation |
## From abstract interpretation to small-step typing
Patrick Cousot is well known for abstract interpretation, which among other
applications offers a general approach to understanding and designing type
systems. It thus surprises me that his work seems to have been discussed only
cursorily on LtU.
Patrick Cousot and Radhia Cousot, Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. POPL 1977, 238-252. A program denotes computations in some universe of objects. Abstract interpretation of programs consists in using that denotation to describe computations in another universe of abstract objects, so that the results of abstract execution give some informations on the actual computations. An intuitive example (which we borrow from Sintzoff) is the rule of signs. The text -1515*17 may be undestood to denote computations on the abstract universe {(+), (-), (+-)} where the semantics of arithmetic operators is defined by the rule of signs. The abstract execution -1515*17 ==> -(+)*(+) ==> (-)*(+) ==> (-), proves that -1515+17 is a negative number. Abstract interpretation is concerned by a particlar underlying structure of the usual universe of computations (the sign, in our example). It gives a summay of some facets of the actual executions of a program. In general this summary is simple to obtain but inacurrate (e.g. -1515+17 ==> -(+)+(+) ==> (-)+(+) ==> (+-)). Despite its fundamental incomplete results abstract interpretation allows the programmer or the compiler to answer questions which do not need full knowledge of program executions or which tolerate an imprecise answer (e.g. partial correctness proofs of programs ignoring the termination problems, type checking, program optimizations which are not carried in the absence of certainty about their feasibility, ...).Patrick Cousot, Types as abstract interpretations. POPL 1997, 316-331. Starting from a denotational semantics of the eager untyped lambda-calculus with explicit runtime errors, the standard collecting semantics is defined as specifying the strongest program properties. By a first abstraction, a new sound type collecting semantics is derived in compositional fixpoint form. Then by successive (semi-dual) Galois connection based abstractions, type systems and/or type inference algorithms are designed as abstract semantics or abstract interpreters approximating the type collecting semantics. This leads to a hierarchy of type systems, which is part of the lattice of abstract interpretations of the untyped lambda-calculus. This hierarchy includes two new à la Church/Curry polytype systems. Abstractions of this polytype semantics lead to classical Milner/Mycroft and Damas/Milner polymorphic type schemes, Church/Curry monotypes and Hindley principal typing algorithm. This shows that types are abstract interpretations.
I started learning more about abstract interpretation for two reasons. First,
abstract interpretation underlies CiaoPP,
a program preprocessor mentioned
here that uses the same assertion language for static and dynamic
checking and optimization. Second, on our way to a logical interpretation of
delimited continuations, Oleg and I build a type system using what we call
Manuel Hermenegildo, Germán Puebla, and Francisco Bueno, Using
global analysis, partial specifications, and an extensible assertion
language for program validation and debugging. In We present a framework for the application of abstract interpretation as an aid during program development, rather than in the more traditional application of program optimization. Program validation and detection of errors is first performed statically by comparing (partial) specifications written in terms of assertions against information obtained from static analysis of the program. The results of this process are expressed in the user assertion language. Assertions (or parts of assertions) which cannot be verified statically are translated into run-time tests. The framework allows the use of assertions to be optional. It also allows using very general properties in assertions, beyond the predefined set understandable by the static analyzer and including properties defined by means of user programs. We also report briefly on an implemention of the framework. The resulting tool generates and checks assertions for Prolog, CLP(R), and CHIP/CLP(fd) programs, and integrates compile-time and run-time checking in a uniform way. The tool allows using properties such as types, modes, non-failure, determinancy, and computational cost, and can treat modules separately, performing incremental analysis. In practice, this modularity allows detecting statically bugs in user programs even if they do not contain any assertions.Oleg Kiselyov and Chung-chieh Shan, A substructural type system for delimited continuations. TLCA 2007. We propose type systems that |
## Browse archives## Active forum topics |

## Recent comments

1 hour 33 min ago

3 hours 12 min ago

4 hours 25 sec ago

4 hours 14 min ago

5 hours 12 min ago

5 hours 15 min ago

6 hours 18 min ago

10 hours 15 min ago

19 hours 42 min ago

23 hours 18 min ago