David Aspinall's Publications

Please click on a paper title for a short abstract. Comments and questions about my work are always welcome, please email me at the address below.

(NB: these lists are out of date; I am in progress of updating to a new web site; meanwhile DBLP has a pretty complete list of my work)

• David Aspinall and Jaroslav Sevcik
  Formalising Java's Data Race Free Guarantee
  Theorem Proving in Higher-Order Logics, TPHOLs'07.
  Springer LNCS. To appear.
  Download as pdf.
• David Aspinall, Lennart Beringer, and Alberto Momigliano.
  Optimisation Validation
  Proc. of Compiler Optimization Meets Compiler Verification, COCV 2006.
  ENTCS vol 176-3, 2007.
  Download as pdf.
• David Aspinall and Kenneth MacKenzie.
  Mobile Resource Guarantees and Policies
  Proc. Intl. Workshop on Construction and Analysis of Safe, Secure and Interoperable Smart Devices (CASSIS 2005). Nice, 2005. LNCS 3956, pp 16-36. 2006.
  Download as pdf.
• David Aspinall, Lennart Beringer, Martin Hofmann, Hans-Wolfgang Loidl and Alberto Momigliano.
  A Program Logic for Resource Verification.
  Proc. of 17th International Conference on Theorem Proving in Higher Order Logics (TPHOLs2004).
  Download as pdf.
• David Aspinall, Stephen Gilmore, Martin Hofmann, Donald Sannella and Ian Stark.
  Mobile Resource Guarantees for Smart Devices.
  Proc. Intl. Workshop on Construction and Analysis of Safe, Secure and Interoperable Smart Devices (CASSIS 2004). Marseille, 2004.
  Download as pdf.
• David Aspinall and Adriana Compagnoni.
  Heap Bounded Assembly Language.
  Journal of Automated Reasoning (Special Issue on Proof-Carrying Code), Volume 31, Issue 3-4, Sep 2003, pp 261-302.
  Download as ps or pdf (pre-final version).

• David Aspinall, Christoph Lüth and Daniel Winterstein.
  A Framework for Interactive Proof
  Towards Mechanized Mathematical Assistants, Manuel Kauers, Manfred Kerber, Robert Miner, Wolfgang Windsteiger (eds).
  Springer LNAI 4573, p. 161--175, 2007.
  Download as pdf.
• David Aspinall, Christoph Lüth and Burkhart Wolff.
  Assisted Proof Document Authoring
  Mathematical Knowledge Management 2005 (MKM '05), Springer LNAI 3863, p. 65--80, 2005.
  Download as pdf.
• Daniel Winterstein, David Aspinall and Christoph Lüth.
  Proof General / Eclipse: A Generic Interface for Interactive Proof.
  Poster paper in IJCAI 2005, pp1587-1588.
  Download as pdf.
• David Aspinall, Christoph Lüth and Daniel Winterstein.
  Parsing, Editing, Proving: The PGIP Display Protocol.
  Presented at International Workshop on User Interfaces for Theorem Provers 2005 (UITP'05).
  Download as pdf.
• Daniel Winterstein, David Aspinall and Christoph Lüth.
  Eclipse Proof General: A Generic Interface for Interactive Proof.
  Presented at International Workshop on User Interfaces for Theorem Provers 2005 (UITP'05).
  Download as pdf.
• David Aspinall and Christoph Lüth. Proof General meets IsaWin.
  Proc. User Interfaces for Theorem Provers 2003 (UITP'03) September 2003, Rome, Italy. Extended version published in ENTCS, 103, 2004, pp3-26.
  Download as pdf.
• David Aspinall Proof General - A Generic Tool for Proof Development.
  Tool description. Appears in Proc. TACAS 2000, LNCS 1785.
  Download as gzipped ps or pdf.
  Also available: some slides used in the presentation of Proof General.

• David Aspinall, Martin Hofmann and Michal Konecny.
  A Type System with Usage Aspects
  Extended version of ESOP 2002 paper with detailed proofs and type reconstruction algorithm.
  To appear in J. Functional Programming, vol 490, 2007.
  Download as pdf.
• David Aspinall and Martin Hofmann.
  Dependent Types.
  Chapter 2 of Advanced Topics in Types and Programming Languages, edited by B. Pierce, MIT Press 2005. pp 45-86.
  Some resources and errata are available.
• David Aspinall and Martin Hofmann.
  Another type system for in-place update.
  Appears in ESOP 2002.
  Download as gzipped ps or pdf. Also available: slides.
• David Aspinall.
  Subtyping with Power Types.
  In Proc. Computer Science Logic, CSL 2000, Fischbachau, Germany. LNCS 186, p.156-171, Springer, 2000.
  Download as gzipped ps or pdf.
  Also available: a draft long version (ps)
• David Aspinall and Adriana Compagnoni.
  Subtyping Dependent Types.
  Appears in TCS, 2001. Download as dvi, gzipped ps or pdf.
  
• David Aspinall and Adriana Compagnoni.
  Subtyping Dependent Types (summary).
  In Proc. Logic In Computer Science, IEEE, 1996.
  Download as ps.
  
• David Aspinall.
  Subtyping with Singleton Types.
  In Proc. Computer Science Logic, CSL'94, Kazimierz, Poland. LNCS 933, p.1-15, Springer, 1995.
  Download as gzipped ps or gzipped dvi.

• David Aspinall, and Piotr Hoffman.
  Datatypes in Memory
  Algebra and Coalgebra in Computer Science, 2nd Conf., CALCO 2007. Ugo Montanari, Till Mossakowski (eds).
  Springer LNCS, 2007.
  Download as pdf.
• David Aspinall.
  Type checking Parametrised Programs and Specifciations in ASL+FPC.
  In Recent Trends in Algebraic Development Techniques, Springer LNCS 2755, 2002.
  Download as pdf.
• David Aspinall and Donald Sannella.
  From Specifications to Code in CASL.
  Appears in AMAST 2002.
  Download as gzipped ps or pdf.
• David Aspinall.
  Types, Subtypes and ASL+.
  In Recent Trends in Data Type Specification, E. Astesiano, G. Reggio and A. Tarlecki (Eds). Springer LNCS 906, 1995.
  Download as gzipped ps or gzipped dvi.

A complete list of my publications is available on request.