| 2004 | Modal Proofs as Distributed Programs (Extended Abstract). | Limin Jia, David Walker |
| 2004 | Call-by-Value Mixin Modules: Reduction Semantics, Side Effects, Types. | Tom Hirschowitz, Xavier Leroy, J. B. Wells |
| 2004 | A Hardest Attacker for Leaking References. | Ren Rydhof Hansen |
| 2004 | Trust Management in Strand Spaces: A Rely-Guarantee Method. | Joshua D. Guttman, F. Javier Thayer, Jay A. Carlson, Jonathan C. Herzog, John D. Ramsdell, Brian T. Sniffen |
| 2004 | Adaptive Pattern Matching on Binary Data. | Per Gustafsson, Konstantinos Sagonas |
| 2004 | Semantical Analysis of Specification Logic, 3: An Operational Approach. | Dan R. Ghica |
| 2004 | Functors for Proofs and Programs. | Jean-Christophe Fillitre, Pierre Letouzey |
| 2004 | Static Analysis of Digital Filters. | Jrme Feret |
| 2004 | A Memoizing Semantics for Functional Logic Languages. | Salvador Espaa Boquera, Vicent Estruch |
| 2004 | Linear Types for Packet Processing. | Robert Ennals, Richard Sharp, Alan Mycroft |
| 2004 | Sound and Decidable Type Inference for Functional Dependencies. | Gregory J. Duck, Simon L. Peyton Jones, Peter J. Stuckey, Martin Sulzmann |
| 2004 | From Constraints to Finite Automata to Filtering Algorithms. | Mats Carlsson, Nicolas Beldiceanu |
| 2004 | System E: Expansion Variables for Flexible Typing with Linear and Non-linear Types and Intersection Types. | Sbastien Carlier, Jeff Polakow, J. B. Wells, A. J. Kfoury |
| 2004 | ML-Like Inference for Classifiers. | Cristiano Calcagno, Eugenio Moggi, Walid Taha |
| 2004 | Extracting a Data Flow Analyser in Constructive Logic. | David Cachera, Thomas P. Jensen, David Pichardie, Vlad Rusu |
| 2004 | Compositional Analysis of Authentication Protocols. | Michele Bugliesi, Riccardo Focardi, Matteo Maffei |
| 2004 | ULM: A Core Programming Model for Global Computing: (Extended Abstract). | Grard Boudol |
| 2004 | Just Fast Keying in the Pi Calculus. | Martn Abadi, Bruno Blanchet, Cdric Fournet |
| 2003 | Building Certified Libraries for PCC: Dynamic Storage Allocation. | Dachuan Yu, Nadeem Abdul Hamid, Zhong Shao |
| 2003 | Verifying Temporal Heap Properties Specified via Evolution Logic. | Eran Yahav, Thomas W. Reps, Shmuel Sagiv, Reinhard Wilhelm |
| 2003 | Rule Formats for Non Interference. | Simone Tini |
| 2003 | Finite Differencing of Logical Formulas for Static Analysis. | Thomas W. Reps, Shmuel Sagiv, Alexey Loginov |
| 2003 | Correctness of Data Representations Involving Heap Data Structures. | Uday S. Reddy, Hongseok Yang |
| 2003 | Register Allocation by Proof Transformation. | Atsushi Ohori |
| 2003 | The Rely-Guarantee Method in Isabelle/HOL. | Leonor Prensa Nieto |