Papers written by Torben Amtoft

some jointly with co-authors, including Andrew Appel, Anindya Banerjee, Assaf J. Kfoury, David Clark, Edwin Rodriguez, Flemming Nielson, Franklyn Turbak, Hanne Riis Nielson, Henning Makholm, Jesper Larsson Träff, Joe B. Wells, John Hatcliff, Kelly Androutsopoulos, Lennart Beringer, Mark Harman, Matt Dwyer, Neil D. Jones, Olivier Danvy, Robby, Robert Muller, Santiago M. Pericas-Geertsen, Venkatesh Prasad Ranganath, Xinming Ou, Zheng Li.

The versions given here are not necessarily identical to any of the previously published ones. I believe that the technical contents are the same. The documents distributed by this server have been provided as a means to ensure timely dissemination of scholarly and technical work on a noncommercial basis. Copyright and all rights therein are maintained by the authors or by other copyright holders, notwithstanding that they have offered their works here electronically. It is understood that all persons copying this information will adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without the explicit permission of the copyright holder.

Correctness of Slicing Finite State Machines Abstract
BibTeX
UCL Research Note in pdf
Presentation in pdf
A Certificate Infrastructure for Machine-Checked Proofs of Conditional Information Flow Abstract
BibTeX
POST'12 in pdf (© Springer-Verlag)
Presentation in pdf
An Alternative Characterization of Weak Order Dependence Abstract
BibTeX
Short paper in pdf
Precise and Automated Contract-based Reasoning for Verification and Certification of Information Flow Properties of Programs with Arrays Abstract
BibTeX
Preliminary full paper in pdf
ESOP'10 in pdf (© Springer-Verlag)
Presentation in pdf
Specification and Checking of Software Contracts for Conditional Information Flow Abstract
BibTeX
SAnToS report (draft) in pdf
FM'08 in pdf (© Springer-Verlag)
Slicing for Modern Program Structures: a Theory for Eliminating Irrelevant Loops Abstract
BibTeX
KSU Report in pdf
IPL 2007 in pdf
Presentation in pdf
Verification Condition Generation for Conditional Information Flow Abstract
BibTeX
KSU Report in pdf
FMSE'07 in pdf ( © ACM )
Presentation in pdf
Flow-sensitive Type Systems and the Ambient Calculus Abstract
BibTeX
Full paper in pdf
Short paper in pdf

This summarizes, and puts into perspective, Causal Type System for Ambient Movements.
A Logic for Information Flow in Object-Oriented Programs Abstract
BibTeX
Full paper in pdf
POPL 2006 in ps, pdf ( © ACM )
Presentation in pdf
A Logic for Information Flow Analysis with an Application to Forward Slicing of Simple Imperative Programs Abstract
BibTeX
SCP 2007 in ps, pdf

This is a further development of Information Flow Analysis in Logical Form.
A New Foundation For Control-Dependence and Slicing for Modern Program Structures Abstract
BibTeX
TOPLAS (almost final) in ps, pdf
ESOP 2005 in ps, pdf (© Springer-Verlag)
Presentation in pdf
Information Flow Analysis in Logical Form Abstract
BibTeX
KSU Report in ps, pdf
SAS 2004 (extended version) in ps, pdf (© Springer-Verlag)
Presentation in pdf
PolyA: True Type Polymorphism for Mobile Ambients Abstract
BibTeX
Full paper in ps, pdf
TCS 2004 in ps, pdf

This is a further development of Mobile Processes with Dependent Communication Types and Singleton Types for Names and Capabilities.
Inferring Annotated Types for Inter-procedural Register Allocation with Constructor Flattening Abstract
BibTeX
TLDI 2003 in ps, pdf ( © ACM )
Presentation in ppt
Mobile Processes with Dependent Communication Types and Singleton Types for Names and Capabilities Abstract
BibTeX
Short paper in ps, pdf
Presentation in pdf
Causal Type System for Ambient Movements Abstract
BibTeX
KSU Report in pdf
Short paper in ps, pdf
Presentation in pdf
Orderly Communication in the Ambient Calculus Abstract
BibTeX
CLSS in pdf

This journal version of What are Polymorphically-Typed Ambients? contains the core features only, yet complete.
What are Polymorphically-Typed Ambients? Abstract
BibTeX
BU Report in ps, pdf
ESOP 2001 in ps, pdf ( © Springer-Verlag )
Presentation in ps, pdf, ps(4)
The Abstraction and Instantiation of String-Matching Programs Abstract
BibTeX
Full paper in pdf
Faithful Translations between Polyvariant Flows and Polymorphic Types Abstract
BibTeX
Draft of full paper in pdf
ESOP 2000 in ps, pdf ( © Springer-Verlag )
Presentation in ps, pdf
Partial Evaluation for Constraint-Based Program Analyses Abstract
BibTeX
BRICS Report in ps, pdf
Type and Effect Systems: Behaviours for Concurrency Abstract
BibTeX
Monograph
Behaviour Analysis for Validating Communication Patterns Abstract
BibTeX
STTT 1998 in ps, pdf
Presentation in pdf
Behaviour Analysis and Safety Conditions: a Case Study in CML Abstract
BibTeX
FASE 1998 in ps, pdf ( © Springer-Verlag )
Polymorphic Subtyping for Effect Analysis: the Static Semantics Abstract
BibTeX
Short paper in ps, pdf ( © Springer-Verlag )
Polymorphic Subtyping for Effect Analysis: the Dynamic Semantics Abstract
BibTeX
Short paper in ps, pdf ( © Springer-Verlag )
Polymorphic Subtyping for Effect Analysis: the Algorithm Abstract
BibTeX
Short paper in ps, pdf ( © Springer-Verlag )
Type and Behaviour Reconstruction for Higher-Order Concurrent Programs Abstract
BibTeX
JFP 1997 in ps, pdf
Local Type Reconstruction by means of Symbolic Fixed Point Iteration Abstract
BibTeX
ESOP 1994 in ps, pdf ( © Springer-Verlag )
Strictness Types: An Inference Algorithm and an Application Abstract
BibTeX
DAIMI Report in ps, pdf

This report covers Minimal Thunkification as well as Local Type Reconstruction by means of Symbolic Fixed Point Iteration
Minimal Thunkification Abstract
BibTeX
WSA 1993 in ps, pdf ( © Springer-Verlag )
Presentation in ps, pdf
Sharing of Computations Abstract
BibTeX
PhD Thesis, 1993 in ps, pdf
Unfold/fold Transformations Preserving Termination Properties Abstract
BibTeX
PLILP 1992 in ps, pdf ( © Springer-Verlag )
Properties of Unfolding-based Meta-level Systems Abstract
BibTeX
PEPM 1991 in ps, pdf
Partial Memoization for obtaining Linear Time Behavior of a 2DPDA Abstract
BibTeX
TCS 1992
Experiments with Implementations of Two Theoretical Constructions Abstract
BibTeX
Botik 1989 in pdf
Memoization and its use in Lazy and Incremental Program Generation Abstract
BibTeX
M.Sc Thesis, 1989 in pdf