Table of Contents
Type inference as abstract interpreter
Types as abstract interpretations
Our experiment
The language: syntax
Concrete semantics
Semantic domains
Semantic evaluation function
Primitive operations 1
Primitive operations 2
Examples 1
Examples 2
Examples 3
Examples 4
From the concrete to the collecting semantics
From the collecting to the abstract semantics
Type abstract interpreter 1
Monotypes with variables
Concrete and abstract domains
Concretization function
Abstraction function
The abstraction of functions
Type variables
Towards constraints
The real abstract domain
Two abstract operations
Merge and function application
Abstract least fixpoint computation
Abstract least fixpoint computation
Mutual recursion
Abstract least fixpoint computation
Examples 1: non-termination
2: “easy” recursion
3: non-typable Cousot’s function
3: failure in widening
4: successful widening loses precision
5: no let-polymorphism
Polymorphism 1
Polymorphism 2
Towards polymorphism
Parametric polytypes 1
Parametric polytypes 2
Type abstract interpreter 2
Some abstract operations
Let-polymorphism
Typings
Examples 1
Examples 2
Examples 3
Examples 4
Type abstract interpreter 3
Abstract semantics of recursive functions
Generalizations
Examples 1
Examples 2
No polymorphic abstraction
Relation to type systems
The Damas-Milner’s type system
The Damas-Milner’s type system 2
Type systems vs. abstract interpreters
|