research
Table of Contents
I am working at ETH Zürich as a postdoc in Peter Müller's group in the area of program verification. I am mainly interested in specifying and verifying object-oriented programs, in ways which can be supported by tools which are both automatic and ultimately usable by typical programmers.
My CV can be found here.
I am on the Programme Committee for OOPSLA 2013.
Papers
2013
- An automatic encoding from VeriFast Predicates into Implicit Dynamic Frames Pdf (submitted)
- Daniel Jost and Alexander J. Summers
- A Formal Semantics for Isorecursive and Equirecursive State Abstractions Pdf
- To appear at ECOOP 2013
- Verification Condition Generation for Permission Logics with Abstract Predicates and Abstraction Functions Pdf
- To appear at ECOOP 2013
- Abstract Read Permissions: Fractional Permissions without the Fractions Pdf
- Presented at VMCAI 2013
2012
- The Relationship Between Separation Logic and Implicit Dynamic Frames Pdf
- Extended version of ESOP 2011 paper below (Pdf)
- Published in Logical Methods in Computer Science
2011
- Freedom Before Commitment - A Lightweight Type System for Object Initialisation Pdf
- Presented at OOPSLA/SPLASH 2011
- see also the (slightly outdated) Technical Report (Jan 2011), ETH Zurich
- Fractional Permissions Without the Fractions Pdf
- Presented at FTfJP 2011
- see also the slides (pptx)
- The Relationship Between Separation Logic and Implicit Dynamic Frames Pdf
- Presented at ESOP 2011
- see also the slides (pptx)
2010
- Towards a Semantic Model for Wildcards Pdf
- Presented at FTfJP 2010
- See also the slides (ppt)
- Considerate Reasoning and the Composite Design Pattern Pdf
- Presented at VMCAI 2010
- See also the Boogie2 code (zip)
- Soundness and Principal Contexts for a Shallow Polymorphic Type System based on Classical Logic Pdf
2009
- The Need for Flexible Object Invariants Pdf
- Presented at IWACO 2009
- Modelling Java Requires State Pdf
- Presented at FTfJP 2009
- Universe-Type-Based Verification Techniques for Mutable Static Fields and Methods Pdf
- Size Does Matter: Two Certified Abstractions to Disprove Entailment in Intuitionistic and Classical Separation Logic Pdf
- Presented at IWACO 2009
2008
- A Universe-Type-Based Verification Technique for Mutable Static Fields and Methods Pdf
- Presented at FTfJP 2008
- See also the extended version (also above)
- A Unified Framework for Verification Techniques for Object Invariants Pdf
- Presented at ECOOP 2008
- See also the full version (submitted)
- Universe Types for Topology and Encapsulation Pdf
- Published in LNCS: Post-proceedings FMCO 2007
- Curry-Howard Term Calculi for Gentzen-Style Classical Logics (PhD Thesis) Pdf
- First supervisor : Steffen van Bakel
- Second supervisor: Luca Cardelli.
2007
- Pandora: A Reasoning Toolbox using Natural Deduction Style Pdf
2006
- On the Computational Representation of Classical Logical Connectives Pdf
- Presented at DCM 2006, Published in ENTCS special issue
- See also the slides
- Approaches to Polymorphism in Classical Sequent Calculus Pdf
- Presented at ESOP 2006
- Pandora - Natural Deduction made Easy Pdf
- Presented at ICTTL 2006
Selected Talks
- The Relationship Between Separation Logic and Implicit Dynamic Frames slides (pptx) (pdf)
- Invited talk at Imperial College London (extension of presentation at ESOP 2011)
- Based on joint work with Matthew Parkinson
- (See also the paper (pdf))
- A Considerate Specification of the Composite Pattern slides (ppt) slides (pdf)
- Presented at 3rd MC and WG meeting of COST action IC0701
- Natural Delimited Control: A Curry-Howard Correspondence for a Canonical Classical Natural Deduction slides (ppt)
- Invited talk at the British Logic Colloquium 2009
- (See also my thesis, Chapters 5 and 6)
- On the Computational Representation of Classical Logical Connectives slides(ppt)
Useful Things
research.txt · Last modified: 2013/05/16 19:57 by alex
Page Tools
