Publications
Drafts
+ James Brotherston, Cristiano Calcagno
Classical BI: Its Semantics and Proof Theory
Submitted.
+ Cristiano Calcagno, Dino Distefano, Viktor Vafeiadis
Compositional Resource Invariant Synthesis
Submitted.
+ Etienne Lozes, Jules Villard, Cristiano Calcagno
Proving Copyless Message Passing
Submitted.
Publications
+ Mohammad Raza, Cristiano Calcagno, Philippa Gardner
Automatic Parallelization using Separation Logic
In Proc. ESOP2009.
+ Martin Nordio, Cristiano Calcagno, Peter Müller, Bertrand Meyer
A Sound and Complete Program Logic for Eiffel
To Appear in TOOLS2009.
+ Cristiano Calcagno, Dino Distefano, Peter O’Hearn, Hongseok Yang
Compositional Shape Analysis by means of BI-Abduction
In Proc. POPL2009.
+ James Brotherston, Cristiano Calcagno
Classical BI (A Logic for Reasoning about Dualising Resource)
In Proc. POPL2009.
+ Hongseok Yang, Oukseh Lee, Cristiano Calcagno, Dino Distefano, Peter O’Hearn
Scalable Shape Analysis for Systems Code
In Proc. CAV2008.
+ James Brotheston, Richard Bornat, Cristiano Calcagno
Cyclic Proofs of Program Termination in Separation Logic
In Proc. POPL2008.
+ Cristiano Calcagno, Thomas Dinstale-Young, Philippa Gardner
Adjunct Elimination in Context Logic for Trees
To Appear in APLAS 2007.
+ Cristiano Calcagno, Matthew Parkinson, Viktor Vafeiadis
Modular Safety Checking for Fine-Grained Concurrency
In Proc. SAS 2007.
+ Cristiano Calcagno, Dino Distefano, Peter O'Hearn, Hongseok Yang
Footprint Analysis: A Shape Analysis that Discovers Preconditions
In Proc. SAS 2007.
+ Cristiano Calcagno, Peter O'Hearn, Hongseok Yang
Local Action and Abstract Separation Logic
In Proc. LICS 2007.
+ J. Berdine, C. Calcagno, B. Cook, D. Distefano, P. O'Hearn, T. Wies, H. Yang
Shape Analysis for Composite Datastructures
In Proc. CAV 2007.
+ Cristiano Calcagno, Philippa Gardner, Uri Zarfaty
Local Reasoning about Data Update
In ENTCS, vol. 172, 2007.
+ Cristiano Calcagno, Philippa Gardner, Uri Zarfaty
Context Logic as Modal Logic: Completeness and Parametric Expressivity
In Proc. POPL 2007.
+ Cristiano Calcagno, Dino Distefano, Peter O'Hearn and Hongseok Yang
Beyond Reachability: Shape Abstraction in the Presence of Pointer Arithmetic
In Proc. SAS 2006.
+ Matthew Parkinson, Richard Bornat, Cristiano Calcagno
Variables as Resource in Hoare Logic
In Proc. LICS 2006.
+ Josh Berdine, Cristiano Calcagno, and Peter O'Hearn
Smallfoot: Modular Automatic Assertion Checking with Separation Logic
In Proc. FMCO 2005.
+ Ik-Soon Kim, Kwangkeun Yi, Cristiano Calcagno
A Polymorphic Modal Type System for Lisp-like Multi-Staged Languages
In Proc. POPL 2006.
+ Josh Berdine, Cristiano Calcagno, Peter O’Hearn
Symbolic Execution with Separation Logic
In Proc. APLAS 2005.
+ Cristiano Calcagno, Philippa Gardner, Matthew Hague
From Separation Logic to First-Order Logic
In Proc. FOSSACS 2005.
+ Cristiano Calcagno, Philippa Gardner, Uri Zarfaty
In Proc. POPL05. (With Proofs).
+ Richard Bornat, Cristiano Calcagno, Peter O’Hearn, Matthew Parkinson
Permission Accounting in Separation Logic
In Proc. POPL05.
+ Cristiano Calcagno, Luca Cardelli, Andrew D. Gordon
Deciding Validity in a Spatial Logic for Trees
@CUP. In Journal of Functional Programming Volume 15, Issue 04, July 2005.
+ Josh Berdine, Cristiano Calcagno, Peter O’Hearn
A Decidable Fragment of Separation Logic
In Proc. FSTTCS 2004. (With Proofs).
+ Cristiano Calcagno, Eugenio Moggi, Walid Taha
ML-Like Inference for Classifiers
In Proc. ESOP 2004.
+ Richard Bornat, Cristiano Calcagno, Peter O’Hearn
Local Reasoning, Separation and Aliasing
In Proc. SPACE 2004.
+ Cristiano Calcagno, Walid Taha, Liwen Huang, Xavier Leroy
Implementing Multi-stage Languages Using ASTs, Gensym and Reflection
In Proc. GPCE 2003.
+ Cristiano Calcagno, Luca Cardelli, Andrew D. Gordon
Deciding Validity in a Spatial Logic for Trees
In Proc. TLDI 2003.
+ Cristiano Calcagno, Peter O'Hearn, Richard Bornat
Program Logic and Equivalence in the Presence of Garbage Collection
@Elsevier Scrience B.V. In Theoretical Computer Science, vol. 298/3, pp557-581.
+ Cristiano Calcagno, Hongseok Yang, Peter O'Hearn
Computability and Complexity Results for a Spatial Assertion Language for Data Structures
@Springer-Verlag. In Proc. FSTTCS 2001. (With Proofs).
+ Cristiano Calcagno, Eugenio Moggi, Tim Sheard
Closed Types for a Safe Imperative MetaML
@CUP. In Journal of Functional Programming Volume 13, Issue 03, May 2003.
+ Cristiano Calcagno, Simon Helsen, Peter Thiemann
Syntactic Type Soundness Results for the Region Calculus
@Academic Press. In Information and Computation Vol. 173, 2002.
+ Cristiano Calcagno, Peter O'Hearn
@Springer-Verlag. In Proc. FOSSACS 2001.
+ Cristiano Calcagno
Stratified Operational Semantics for Safety and Correctness of the Region Calculus
In Proc. POPL 2001.
+ Cristiano Calcagno, Eugenio Moggi
Multi-Stage Imperative Languages: A Conservative Extension Result
@Springer-Verlag. In Proc. SAIG00 WS (PLI) 2000.
+ Cristiano Calcagno, Samin Ishtiaq, Peter O'Hearn
Semantic Analysis of Pointer Aliasing, Allocation and Disposal in Hoare Logic
In Proc. PPDP 2000.
+ Cristiano Calcagno, Eugenio Moggi, Walid Taha
Closed Types as a Simple Approach to Safe Imperative Multi-Stage Programming
@Springer-Verlag. In Proc. ICALP 2000.
+ Cristiano Calcagno
Two-Level Languages for Program Optimization
@Elsevier Scrience B.V. In Theoretical Computer Science, vol. 315, Issue 1, 2004.
Thesis
+ Cristiano Calcagno
Semantic and Logical Properties of Stateful Programming
Technical Report, University of Genova, DISI-TH-2002.
