BibSLEIGH
BibSLEIGH corpus
BibSLEIGH tags
BibSLEIGH bundles
BibSLEIGH people
EDIT!
CC-BY
Open Knowledge
XHTML 1.0 W3C Rec
CSS 2.1 W3C CanRec
email twitter
Travelled to:
1 × Canada
1 × Cyprus
1 × Denmark
1 × France
1 × Korea
1 × Poland
1 × Slovenia
2 × Germany
2 × Italy
2 × Switzerland
3 × Spain
3 × United Kingdom
8 × USA
Collaborated with:
P.W.O'Hearn H.Yang P.Gardner D.Distefano S.v.Staden E.Moggi B.Meyer R.Bornat M.J.Parkinson W.Taha J.Brotherston M.Nordio U.Zarfaty P.Müller C.A.Furia J.Villard É.Lozes M.Raza V.Vafeiadis I.Kim K.Yi M.Hague S.S.Ishtiaq J.Berdine B.Cook L.Huang X.Leroy J.Tschannen O.Lee T.Wies
Talks about:
logic (15) analysi (6) separ (6) shape (5) multi (5) program (4) stage (4) abstract (3) languag (3) system (3)

Person: Cristiano Calcagno

DBLP DBLP: Calcagno:Cristiano

Contributed to:

FASE 20132013
POPL 20122012
ECOOP 20102010
OOPSLA 20102010
TACAS 20102010
TOOLS Europe 20102010
ESOP 20092009
POPL 20092009
TOOLS Europe 20092009
CAV 20082008
LOPSTR 20082008
POPL 20082008
CAV 20072007
LICS 20072007
POPL 20072007
SAS 20072007
LICS 20062006
POPL 20062006
SAS 20062006
FoSSaCS 20052005
POPL 20052005
ESOP 20042004
GPCE 20032003
FoSSaCS 20012001
POPL 20012001
ICALP 20002000
PPDP 20002000
SAIG 20002000

Wrote 31 papers:

FASE-2013-NordioCF #javascript #named #verification
Javanni: A Verifier for JavaScript (MN, CC, CAF), pp. 231–234.
POPL-2012-StadenCM
Freefinement (SvS, CC, BM), pp. 7–18.
ECOOP-2010-StadenCM #execution #logic #object-oriented #specification #verification
Verifying Executable Object-Oriented Specifications with Separation Logic (SvS, CC, BM), pp. 151–174.
OOPSLA-2010-StadenC #abstraction #multi #reasoning
Reasoning about multiple related abstractions with MultiStar (SvS, CC), pp. 504–519.
TACAS-2010-VillardLC
Tracking Heaps That Hop with Heap-Hop (JV, ÉL, CC), pp. 275–279.
TOOLS-EUROPE-2010-NordioCMMT #reasoning
Reasoning about Function Objects (MN, CC, BM, PM, JT), pp. 79–96.
ESOP-2009-RazaCG #automation #logic #parallel
Automatic Parallelization with Separation Logic (MR, CC, PG), pp. 348–362.
POPL-2009-BrotherstonC #logic #reasoning
Classical BI: a logic for reasoning about dualising resources (JB, CC), pp. 328–339.
POPL-2009-CalcagnoDOY #analysis #composition
Compositional shape analysis by means of bi-abduction (CC, DD, PWO, HY), pp. 289–300.
TOOLS-EUROPE-2009-NordioCMM #eiffel #logic
A Sound and Complete Program Logic for Eiffel (MN, CC, PM, BM), pp. 195–214.
CAV-2008-YangLBCCDO #analysis #scalability
Scalable Shape Analysis for Systems Code (HY, OL, JB, CC, BC, DD, PWO), pp. 385–398.
LOPSTR-2008-CalcagnoDOY
Space Invading Systems Code (CC, DD, PWO, HY), pp. 1–3.
POPL-2008-BrotherstonBC #logic #proving #termination
Cyclic proofs of program termination in separation logic (JB, RB, CC), pp. 101–112.
CAV-2007-BerdineCCDOWY #analysis #data type
Shape Analysis for Composite Data Structures (JB, CC, BC, DD, PWO, TW, HY), pp. 178–192.
LICS-2007-CalcagnoOY #logic
Local Action and Abstract Separation Logic (CC, PWO, HY), pp. 366–378.
POPL-2007-CalcagnoGZ #logic #parametricity
Context logic as modal logic: completeness and parametric inexpressivity (CC, PG, UZ), pp. 123–134.
SAS-2007-CalcagnoDOY #analysis
Footprint Analysis: A Shape Analysis That Discovers Preconditions (CC, DD, PWO, HY), pp. 402–418.
SAS-2007-CalcagnoPV #composition #concurrent #fine-grained #safety
Modular Safety Checking for Fine-Grained Concurrency (CC, MJP, VV), pp. 233–248.
LICS-2006-ParkinsonBC #hoare #logic
Variables as Resource in Hoare Logics (MJP, RB, CC), pp. 137–146.
POPL-2006-KimYC #multi #polymorphism #type system
A polymorphic modal type system for lisp-like multi-staged languages (ISK, KY, CC), pp. 257–268.
SAS-2006-CalcagnoDOY #abstraction #pointer #reachability
Beyond Reachability: Shape Abstraction in the Presence of Pointer Arithmetic (CC, DD, PWO, HY), pp. 182–203.
FoSSaCS-2005-CalcagnoGH #first-order #logic
From Separation Logic to First-Order Logic (CC, PG, MH), pp. 395–409.
POPL-2005-BornatCOP #logic
Permission accounting in separation logic (RB, CC, PWO, MJP), pp. 259–270.
POPL-2005-CalcagnoGZ #logic
Context logic and tree update (CC, PG, UZ), pp. 271–282.
ESOP-2004-CalcagnoMT #classification
ML-Like Inference for Classifiers (CC, EM, WT), pp. 79–93.
GPCE-2003-CalcagnoTHL #abstract syntax tree #implementation #multi #using
Implementing Multi-stage Languages Using ASTs, Gensym, and Reflection (CC, WT, LH, XL), pp. 57–76.
FoSSaCS-2001-CalcagnoO #logic #on the
On Garbage and Program Logic (CC, PWO), pp. 137–151.
POPL-2001-Calcagno #calculus #correctness #safety #semantics
Stratified operational semantics for safety and correctness of the region calculus (CC), pp. 155–165.
ICALP-2000-CalcagnoMT #approach #imperative #multi #programming
Closed Types as a Simple Approach to Safe Imperative Multi-stage Programming (CC, EM, WT), pp. 25–36.
PPDP-2000-CalcagnoIO #alias #analysis #hoare #logic #pointer #semantics
Semantic analysis of pointer aliasing, allocation and disposal in Hoare logic351292 (CC, SSI, PWO), pp. 190–201.
SAIG-2000-CalcagnoM #imperative #multi
Multi-Stage Imperative Languages: A Conservative Extension Result (CC, EM), pp. 92–107.

Bibliography of Software Language Engineering in Generated Hypertext (BibSLEIGH) is created and maintained by Dr. Vadim Zaytsev.
Hosted as a part of SLEBOK on GitHub.