David Aspinall
David Aspinall
Professor in Computer Science, University of Edinburgh
Verified email at ed.ac.uk
TitleCited byYear
Proof General: A generic tool for proof development
D Aspinall
International Conference on Tools and Algorithms for the Construction and…, 2000
1902000
On validity of program transformations in the Java memory model
J Ševčk, D Aspinall
European Conference on Object-Oriented Programming, 27-51, 2008
1562008
Personal choice and challenge questions: a security and usability assessment
M Just, D Aspinall
Proceedings of the 5th Symposium on Usable Privacy and Security, 8, 2009
1042009
Subtyping with singleton types
D Aspinall
International Workshop on Computer Science Logic, 1-15, 1994
821994
Mobile resource guarantees for smart devices
D Aspinall, S Gilmore, M Hofmann, D Sannella, I Stark
International Workshop on Construction and Analysis of Safe, Secure, and…, 2004
812004
Subtyping dependent types
D Aspinall, A Compagnoni
Proceedings 11th Annual IEEE Symposium on Logic in Computer Science, 86-97, 1996
791996
Formalising Java’s data race free guarantee
D Aspinall, J Ševčk
International Conference on Theorem Proving in Higher Order Logics, 22-37, 2007
742007
Data driven authentication: On the effectiveness of user behaviour modelling with mobile device sensors
HG Kayacik, M Just, L Baillie, D Aspinall, N Micallef
arXiv preprint arXiv:1410.7743, 2014
652014
Another type system for in-place update
D Aspinall, M Hofmann
European Symposium on Programming, 36-52, 2002
652002
A program logic for resources
D Aspinall, L Beringer, M Hofmann, HW Loidl, A Momigliano
Theoretical Computer Science 389 (3), 411-445, 2007
642007
Subtyping dependent types
D Aspinall, A Compagnoni
Theoretical Computer Science 266 (1-2), 273-309, 2001
532001
Heap-bounded assembly language
D Aspinall, A Compagnoni
Journal of automated reasoning 31 (3-4), 261-302, 2003
482003
A program logic for resource verification
D Aspinall, L Beringer, M Hofmann, HW Loidl, A Momigliano
International Conference on Theorem Proving in Higher Order Logics, 34-49, 2004
452004
A framework for interactive proof
D Aspinall, C Lth, D Winterstein
Towards Mechanized Mathematical Assistants, 161-175, 2007
422007
Dependent types
D Aspinall, M Hofmann
Advanced Topics in Types and Programming Languages, 45-86, 2005
422005
Java memory model examples: Good, bad and ugly
D Aspinall, J Sevcik
Proc. of VAMP 7, 2007
392007
Mobile resource guarantees and policies
D Aspinall, K MacKenzie
International Workshop on Construction and Analysis of Safe, Secure, and…, 2005
302005
Towards formal proof script refactoring
I Whiteside, D Aspinall, L Dixon, G Grov
International Conference on Intelligent Computer Mathematics, 260-275, 2011
292011
Type systems for modular programs and specifications
DR Aspinall
University of Edinburgh, 1997
271997
Proof general
D Aspinall, T Kleymann
252011
The system can't perform the operation now. Try again later.
Articles 1–20