Type-Based Analysis and Applications
Jens Palsberg
Type-based analysis is an approach to static analysis of programs
that has been studied for more than a decade.
A type-based analysis assumes that the program type checks,
and the analysis takes advantage of that.
This website is a resource for researchers of type-based analysis.
It contains links to papers in the area, including
a short survey paper,
and slides for a talk based
on the survey paper.
The survey paper examines the state of the art of type-based analysis,
and it surveys some of the many software tools that use type-based analysis.
Most of the surveyed tools use types as discriminators,
while most of the theoretical studies use type and effect systems.
Overall, type-based analysis is a promising approach to achieving
both provable correctness and good performance with a reasonable effort.
Please send information about papers on type-based analysis
that are missing from the list below
to Jens Palsberg.
Papers on Type-Based Analysis
-
A Core Calculus of Dependency,
by Martin Abadi and Anindya Banerjee and Nevin Heintze and Jon Riecke.
In Proceedings of POPL'99, ACM SIGPLAN-SIGACT Symposium on
Principles of Programming Languages, pages 147-160, 1999.
-
Minimal Thunkification,
by Torben Amtoft.
In Proceedings of WSA'93, 3rd International Workshop on Static Analysis,
LNCS 724,
pages 218-229, 1993.
-
Fast Static Analysis of C++ Virtual Function Calls,
by David Bacon and Peter Sweeney.
In Proceedings of OOPSLA'96, ACM SIGPLAN Conference on
Object-Oriented Programming Systems, Languages and Applications,
pages 324-341, 1996.
-
Fast and Effective Optimization of
Statically Typed Object-Oriented Languages,
by David Bacon.
Ph.D. thesis, University of California, Berkeley, 1997.
-
A Modular, Polyvariant and Type-Based Closure Analysis,
by Anindya Banerjee.
In Proceedings of ICFP'97, ACM International Conference on
Functional Programming,
pages 1-10, 1997.
-
Region Analysis and the Polymorphic Lambda Calculus,
by Anindya Banerjee, Nevin Heintze, and Jon G. Riecke.
In Proceedings of LICS'99,
Fourteenth IEEE Symposium on Logic in Computer Science,
pages 88-97, 1999.
-
From Region Inference to von Neumann Machines via
Region Representation Inference,
by Lars Birkedal, Mads Tofte, and Magnus Vejlstrup.
In Proceedings of POPL'96, ACM SIGPLAN-SIGACT Symposium on
Principles of Programming Languages, pages 171-183, 1996.
-
Confined Types,
by Boris Bokowski and Jan Vitek.
In Proceedings of OOPSLA'99, ACM SIGPLAN Conference on
Object-Oriented Programming Systems, Languages and Applications,
pages 82-96, 1999.
-
A Parameterized Type System for Race-Free Java Programs,
by Chandrasekhar Boyapati and Martin Rinard.
In Proceedings of OOPSLA'01, ACM SIGPLAN Conference on
Object-Oriented Programming Systems, Languages and Applications,
2001, to appear.
-
Optimization of Object-Oriented Programs using Static Class
Hierarchy Analysis,
by Jeffrey Dean and David Grove and Craig Chambers.
In Proceedings of ECOOP'95, European Conference on
Object-Oriented Programming,
pages 77-101, 1995.
-
Strongly Typed Flow-Directed Representation Transformations,
by Allyn Dimock, Robert Muller, Franklyn Turbak, and J. B. Wells.
In Proceedings of ICFP'97,
International Conference on Functional Programming,
pages 11-24, 1997.
-
Type-Based Alias Analysis,
by Amer Diwan, Kathryn McKinley, and Eliot Moss.
In Proceedings of PLDI'98, ACM SIGPLAN Conference on
Programming Language Design and Implementation,
pages 106-117, 1998.
-
Unified Analysis of Array and Object References in
Strongly Typed Languages,
by Stephen Fink, and Kathleen Knobe, and Vivek Sarkar.
In Proceedings of SAS'00, International Static Analysis Symposium,
pages 155-174, 2000.
-
Type Systems and Algorithms for Useless-Variable Elimination,
by Adam Fischbach and John Hannan.
In Proceedings of PADO'01, Symposium on Programs as Data Objects,
LNCS 2053, pages 25-38, 2001,
-
Type-Based Race Detection for Java,
by Cormac Flanagan and Stephen Freund.
In Proceedings of PLDI'00, ACM SIGPLAN Conference on
Programming Language Design and Implementation,
pages 219-232, 2000.
-
Refinement Types for ML,
by Tim Freeman.
Ph.D. thesis, Carnegie Mellon University, 1994.
-
Field Analysis: Getting Useful and Low-cost Interprocedural Information,
by Sanjay Ghemawat, Keith Randall, and Daniel Scales.
In Proceedings of PLDI'00, ACM SIGPLAN Conference on
Programming Language Design and Implementation,
pages 334-344, 2000.
-
Encapsulating Objects with Confined Types,
by Christian Grothoff, Jan Vitek, and Jens Palsberg.
In Proceedings of OOPSLA'01, ACM SIGPLAN Conference on
Object-Oriented Programming Systems, Languages and Applications,
2001, to appear.
-
A Usage Analysis with Bounded Usage Polymorphism and Subtyping,
by Jorgen Gustavsson and Josef Svenningsson.
In Proceedings of IFL'00, Implementation of Functional Languages,
2000.
-
Constraint Abstractions,
by Jorgen Gustavsson and Josef Svenningsson.
In Proceedings of PADO'01, Symposium on Programs as Data Objects,
LNCS 2053, 2001,
-
Type Systems for Closure Conversions,
by John Hannan.
In Proceedings of Workshop on Types for Program Analysis,
pages 48-62, 1995.
-
Control-Flow Analysis and Type Systems,
by Nevin Heintze.
In Proceedings of SAS'95, International Static Analysis Symposium,
LNCS 983, pages 189-206, 1995.
-
Linear-time Subtransitive Control Flow Analysis,
by Nevin Heintze and David McAllester.
In Proceedings of PLDI'97, ACM SIGPLAN Conference on
Programming Language Design and Implementation,
pages 261-272, 1997.
-
The SLam Calculus: Programming with Secrecy and Integrity,
by Nevin Heintze and Jon G. Riecke.
In Proceedings of POPL'98, ACM SIGPLAN-SIGACT Symposium on
Principles of Programming Languages, pages 365-377, 1998.
-
A Type System for Bounded Space and Functional In-Place Update,
by Martin Hofmann.
Nordic Journal of Computing, 7(4), Winter 2000.
-
Partial Redundancy Elimination for Access Path Expressions,
by Antony L. Hosking, Nathaniel Nystrom, David Whitlock,
Quintin Cutts, and Amer Diwan.
Software - Practice and Experience 31(6):577-600, 2001.
-
Type-Directed Flow Analysis for Typed Intermediate Languages,
by Suresh Jagannathan, Andrew Wright, and Stephen Weeks.
In Proceedings of SAS'97, International Static Analysis Symposium,
1997.
-
Inference of Polymorphic and Conditional Strictness Properties,
by Thomas Jensen.
In Proceedings of POPL'98, ACM SIGPLAN-SIGACT Symposium on
Principles of Programming Languages, pages 209-221, 1998.
-
Algebraic Reconstruction of Types and Effects,
by Pierre Jouvelot and David Gifford.
In Proceedings of POPL'91, ACM SIGPLAN-SIGACT Symposium on
Principles of Programming Languages, pages 303-310, 1991.
-
Type-Based Useless Variable Elimination,
by Naoki Kobayashi.
In Proceedings of PEPM'00, ACM Symposium on Partial Evaluation and
Semantics-Based Program Manipulation,
pages 84-93, 2000.
-
Types and Concept Analysis for Legacy Systems,
by Tobias Kuipers and Leon Moonen.
In Proceedings of the 8th International Workshop on Program Comprehension,
IEEE Computer Society Press, June 2000.
-
On Strictness and its Analysis,
by Tsung-Min Kuo and Prateek Mishra.
In Proceedings of POPL'87, ACM SIGPLAN-SIGACT Symposium on
Principles of Programming Languages, pages 144-155, 1987.
-
Strictness Analysis: A new Perspective based on Type Inference,
by Tsung-Min Kuo and Prateek Mishra.
In Proceedings of FPCA'89, Conference on
Functional Programming Languages and Computer Architecture
pages 260-272, 1989.
-
An Overview of Types in Compilation,
by Xavier Leroy.
In Proceedings of ACM SIGPLAN Workshop on Types in Compilation,
pages 1-8, 1998.
-
Polymorphic Effect Systems,
by John Lucassen and David Gifford.
In Proceedings of POPL'88, ACM SIGPLAN-SIGACT Symposium on
Principles of Programming Languages, pages 47-57, 1988.
-
A Type-Based Locality Analysis for a Functional Distributed Language,
by Alvaro Moreira.
Ph.D. thesis, University of Edinburgh, 1999.
-
Exact Flow Analysis,
by Christian Mossin.
In Proceedings of SAS'97, International Static Analysis Symposium,
pages 250-264, 1997.
-
Flow Analysis of Typed Higher-Order Languages,
by Christian Mossin.
Ph.D. thesis, University of Copenhagen (DIKU), 1997.
-
Higher-Order Value Flow Graphs,
by Christian Mossin.
Nordic Journal of Computing 5:214-234, 1998.
-
Type and Effect Systems,
by Flemming Nielson and Hanne Riis Nielson.
In Correct System Design,
pages 114-136, 1999.
-
Principles of Program Analysis,
by Flemming Nielson, Hanne Riis Nielson, and Chris Hankin.
Springer-Verlag, 1999.
-
Automatic Binding Time Analysis for a Typed Lambda-Calculus,
by Hanne Riis Nielson and Flemming Nielson.
In Science of Computer Programming 10:139-176, 1988.
-
Trust in the Lambda-Calculus,
by Peter Orbaek and Jens Palsberg.
Journal of Functional Programming 7(6):557-591, November 1997.
-
Type-Based Analysis and Applications,
by Jens Palsberg.
In Proceedings of PASTE'01, ACM SIGPLAN/SIGSOFT
Workshop on Program Analysis for Software Tools, 2001.
To appear.
-
Information Flow Inference for Free
by Francois Pottier and Sylvain Conchon.
In Proceedings of ICFP'00,
ACM SIGPLAN International Conference on Functional Programming,
pages 46-57, 2000.
-
Type-Based Flow Analysis: From Polymorphic Subtyping to CFL-Reachability,
by Jakob Rehof and Manuel Fahndrich.
In Proceedings of POPL'01, ACM SIGPLAN-SIGACT Symposium on
Principles of Programming Languages, pages 54-66, 2001.
-
User-extensible Simplification - Type-based Optimizer Generators,
by Sibylle Schupp, Douglas Gregor, David Musser, and Shin-Ming Liu.
In Proceedings of International Conference on Compiler Construction,
LNCS, pages 86-101, 2001.
-
Type-Directed Continuation Allocation,
by Zhong Shao and Valery Trifonov.
In Proceedings of ACM SIGPLAN Workshop on Types in Compilation,
pages 116-136, 1998.
-
Secure Information Flow in Multi-threaded Imperative Language,
by Geoffrey Smith and Dennis Volpano.
In Proceedings of POPL'98, ACM SIGPLAN-SIGACT Symposium on
Principles of Programming Languages, pages 355-364, 1998.
-
Annotated Type Systems for Program Analysis,
by Kirsten Solberg.
Ph.D. thesis, University of Aarhus, 1995.
-
Strictness and Totality Analysis,
by Kirsten Solberg and Hanne Riis Nielson and Flemming Nielson.
In Proceedings of SAS'94, International Static Analysis Symposium,
LNCS 983, pages 408-422, 1994.
-
Strictness and Totality Analysis with Conjunction,
by Kirsten Solberg and Hanne Riis Nielson and Flemming Nielson.
In Proceedings of TAPSOFT'95, Theory and Practice of Software Development,
LNCS 915, pages 501-515, 1995,
-
Practical Virtual Method Call Resolution for Java,
by Vijay Sundaresan, Laurie Hendren, Chrislain Razafimahefa, Raja Vallee-Rai,
Patrick Lam, Etienne Gagnon, and Charles Godin.
In Proceedings of OOPSLA'00, ACM SIGPLAN Conference on
Object-Oriented Programming Systems, Languages and Applications,
pages 264-280, 2000.
-
Extracting Library-Based Object-Oriented Applications,
by Peter Sweeney and Frank Tip.
In Proceedings of FSE'00, International Symposium on
Foundations of Software Engineering,
pages 98-107, 2000.
-
The Type and Effect Discipline,
by Jean-Pierre Talpin and Pierre Jouvelot.
Information and Computation 111:245-296, 1994.
A preliminary version was presented at LICS'92.
-
Separate Abstract Interpretation for Control-Flow Analysis,
by Yan Mei Tang and Pierre Jouvelot.
In Proceedings of TACS'94, Theoretical Aspects of Computing Software,
pages 224-243, 1994.
-
Effect Systems with Subtyping,
by Yan Mei Tang and Pierre Jouvelot.
In Proceedings of PEPM'95, ACM Symposium on Partial Evaluation and
Sematics-Based Program Manipulation,
pages 45-53, 1995.
-
Formalizing Resource Allocation in a Compiler,
by Peter Thiemann.
In Proceedings of ACM SIGPLAN Workshop on Types in Compilation,
pages 178-194, 1998.
-
Practical Experience with an Application Extractor for Java,
by Frank Tip, Chris Laffra, Peter Sweeney, and David Streeter.
In Proceedings of OOPSLA'99, ACM SIGPLAN Conference on
Object-Oriented Programming Systems, Languages and Applications,
pages 292-305, 1996.
-
Scalable Propagation-Based Call Graph Construction Algorithms,
by Frank Tip and Jens Palsberg.
In Proceedings of OOPSLA'00, ACM SIGPLAN Conference on
Object-Oriented Programming Systems, Languages and Applications,
pages 281-293, 2000.
-
Region-Based Memory Management,
by Mads Tofte and Jean-Pierre Talpin.
Information and Computation 132(2):109-176, 1997.
-
Optimizing ML Using a Hierarchy of Monadic Types,
by Andrew Tolmach.
In Proceedings of ACM SIGPLAN Workshop on Types in Compilation,
pages 97-116, 1998.
-
Compiling with Polymorphic and Polyvariant Flow Types,
by Franklyn Turbak, Allyn Dimock, Robert Muller, and J. B. Wells.
In Proceedings of ACM SIGPLAN Workshop on Types in Compilation,
1997.
-
A Calculus with Polymorphic and Polyvariant Flow Types,
by J. B. Wells, Allyn Dimock, Robert Muller, and Franklyn Turbak.
To appear in Journal of Functional Programming.
-
Typing References by Effect Inference,
by Andrew Wright.
In Proceedings of ESOP'92, European Symposium on Programming,
LNCS 582,
pages 473-491, 1992.
-
Compiling Java to a Typed Lambda-Calculus: A Preliminary Report,
by Andrew Wright, Suresh Jagannathan, Cristian Ungureanu, and Aaron Hertzmann.
In Proceedings of ACM SIGPLAN Workshop on Types in Compilation,
1998.
-
A new Technique for Strictness Analysis,
by David Wright.
In Proceedings of TAPSOFT'91,
LNCS 494,
pages 235-258, 1991.
-
Reasoning about Continuations with Control Effects,
by Pierre Jouvelot and David K. Gifford.
In Proceedings of PLDI'89,
pages 218-226, 1989.
-
From Control Effects to Typed Continuation Passing,
by Hayo Thielecke.
In Proceedings of POPL'03,
pages 139-149, 2003.