2009 |
31 | EE | David Aspinall,
Serge Autexier,
Christoph Lüth,
Marc Wagner:
Towards Merging PlatOmega and PGIP.
Electr. Notes Theor. Comput. Sci. 226: 3-21 (2009) |
2008 |
30 | EE | David Aspinall,
Ewen Denney,
Christoph Lüth:
A Tactic Language for Hiproofs.
AISC/MKM/Calculemus 2008: 339-354 |
29 | EE | Jaroslav Sevcík,
David Aspinall:
On Validity of Program Transformations in the Java Memory Model.
ECOOP 2008: 27-51 |
28 | EE | David Aspinall,
Patrick Maier,
Ian Stark:
Monitoring External Resources in Java MIDP.
Electr. Notes Theor. Comput. Sci. 197(1): 17-30 (2008) |
27 | EE | David Aspinall,
Martin Hofmann,
Michal Konecný:
A type system with usage aspects.
J. Funct. Program. 18(2): 141-178 (2008) |
2007 |
26 | EE | David Aspinall,
Piotr Hoffman:
Datatypes in Memory.
CALCO 2007: 111-125 |
25 | EE | David Aspinall,
Christoph Lüth,
Daniel Winterstein:
A Framework for Interactive Proof.
Calculemus/MKM 2007: 161-175 |
24 | EE | David Aspinall,
Patrick Maier,
Ian Stark:
Safety Guarantees from Explicit Resource Management.
FMCO 2007: 52-71 |
23 | EE | David Aspinall,
Jaroslav Sevcík:
Formalising Java's Data Race Free Guarantee.
TPHOLs 2007: 22-37 |
22 | EE | David Aspinall,
Lennart Beringer,
Alberto Momigliano:
Optimisation Validation.
Electr. Notes Theor. Comput. Sci. 176(3): 37-59 (2007) |
21 | EE | David Aspinall,
Christoph Lüth:
Special Issue on User Interfaces in Theorem Proving: Preface.
J. Autom. Reasoning 39(2): 107-108 (2007) |
20 | EE | David Aspinall,
Lennart Beringer,
Martin Hofmann,
Hans-Wolfgang Loidl,
Alberto Momigliano:
A program logic for resources.
Theor. Comput. Sci. 389(3): 411-445 (2007) |
2006 |
19 | EE | David Aspinall,
Daniel Winterstein,
Christoph Lüth,
Ahsan Fayyaz:
Proof general in Eclipse: system and architecture overview.
ETX 2006: 45-49 |
2005 |
18 | EE | David Aspinall,
Kenneth MacKenzie:
Mobile Resource Guarantees and Policies.
CASSIS 2005: 16-36 |
17 | EE | Daniel Winterstein,
David Aspinall,
Christoph Lüth:
Proof General / Eclipse: A Generic Interface for Interactive Proof.
IJCAI 2005: 1587-1588 |
16 | EE | David Aspinall,
Christoph Lüth,
Burkhart Wolff:
Assisted Proof Document Authoring.
MKM 2005: 65-80 |
15 | | Donald Sannella,
Martin Hofmann,
David Aspinall,
Stephen Gilmore,
Ian Stark,
Lennart Beringer,
Hans-Wolfgang Loidl,
Kenneth MacKenzie,
Alberto Momigliano,
Olha Shkaravska:
Mobile Resource Guarantees (project evaluation paper).
Trends in Functional Programming 2005: 211-226 |
2004 |
14 | EE | David Aspinall,
Stephen Gilmore,
Martin Hofmann,
Donald Sannella,
Ian Stark:
Mobile Resource Guarantees for Smart Devices.
CASSIS 2004: 1-26 |
13 | EE | David Aspinall,
Lennart Beringer,
Martin Hofmann,
Hans-Wolfgang Loidl,
Alberto Momigliano:
A Program Logic for Resource Verification.
TPHOLs 2004: 34-49 |
12 | EE | David Aspinall,
Christoph Lüth:
Preface.
Electr. Notes Theor. Comput. Sci. 103: 1-2 (2004) |
11 | EE | David Aspinall,
Christoph Lüth:
Proof General meets IsaWin: Combining Text-Based And Graphical User Interfaces.
Electr. Notes Theor. Comput. Sci. 103: 3-26 (2004) |
2003 |
10 | EE | David Aspinall,
Adriana B. Compagnoni:
Heap-Bounded Assembly Language.
J. Autom. Reasoning 31(3-4): 261-302 (2003) |
2002 |
9 | EE | David Aspinall,
Donald Sannella:
From Specifications to Code in CASL.
AMAST 2002: 1-14 |
8 | EE | David Aspinall,
Martin Hofmann:
Another Type System for In-Place Update.
ESOP 2002: 36-52 |
7 | EE | David Aspinall:
Type Checking Parametrised Programs and Specifications in ASL+FPC.
WADT 2002: 129-144 |
2001 |
6 | EE | David Aspinall,
Adriana B. Compagnoni:
Subtyping dependent types.
Theor. Comput. Sci. 266(1-2): 273-309 (2001) |
2000 |
5 | EE | David Aspinall:
Subtyping with Power Types.
CSL 2000: 156-171 |
4 | EE | David Aspinall:
Proof General: A Generic Tool for Proof Development.
TACAS 2000: 38-42 |
1996 |
3 | | David Aspinall,
Adriana B. Compagnoni:
Subtyping Dependent Types (Summary).
LICS 1996: 86-97 |
1994 |
2 | | David Aspinall:
Types, Subtypes, and ASL+.
COMPASS/ADT 1994: 116-131 |
1 | | David Aspinall:
Subtyping with Singleton Types.
CSL 1994: 1-15 |