Accepting PhD Students

PhD projects

Please see the Informatics Security and Privacy group page for projects including some of mine: <a href="http://web.inf.ed.ac.uk/security-privacy/phd-study/phd-topics">S and P PhD topics</a>

Please contact me directly for topics in other areas.

If you made any changes in Pure these will be visible here soon.
Filter
Conference contribution

Search results

  • 2009

    Towards a Type System for Security APIs

    Keighren, G., Aspinall, D. & Steel, G., 2009, Foundations and Applications of Security Analysis: Joint Workshop on Automated Reasoning for Security Protocol Analysis and Issues in the Theory of Security, ARSPA-WITS 2009, York, UK, March 28-29, 2009, Revised Selected Papers. Degano, P. & Viganò, L. (eds.). Springer Berlin Heidelberg, p. 173-192 20 p. (Lecture Notes in Computer Science; vol. 5511).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

    Open Access
    File
  • 2008

    Monitoring External Resources in Java MIDP

    Aspinall, D., Maier, P. & Stark, I., 21 Feb 2008, Proceedings of the First International Workshop on Run Time Enforcement for Mobile and Distributed Systems (REM 2007). Vol. 197. p. 17-30 14 p.

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

    Open Access
    File
  • A Tactic Language for Hiproofs

    Aspinall, D., Denney, E. & Lüth, C., 2008, Intelligent Computer Mathematics, 9th International Conference, AISC 2008, 15th Symposium, Calculemus 2008, 7th International Conference, MKM 2008, Birmingham, UK, July 28 - August 1, 2008. Proceedings.: Lecture Notes in Computer Science. Springer Berlin Heidelberg, Vol. 5144. p. 339-354 16 p. (Lecture Notes in Computer Scince; vol. 5144).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  • On Validity of Program Transformations in the Java Memory Model

    Sevcik, J. & Aspinall, D., 2008, ECOOP 2008 — Object-Oriented Programming. Vitek, J. (ed.). Springer-Verlag GmbH, p. 27-51 25 p. (Lecture Notes in Computer Science; vol. 5142).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  • Safety Guarantees from Explicit Resource Management

    Aspinall, D., Maier, P. & Stark, I., 2008, Formal Methods for Components and Objects. de Boer, F., Bonsangue, M., Graf, S. & de Roever, W-P. (eds.). Springer-Verlag GmbH, Vol. 5382. p. 52-71 20 p. (Lecture Notes in Computer Science).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  • 2007

    A Framework for Interactive Proof

    Aspinall, D., Lüth, C. & Winterstein, D., 2007, Towards Mechanized Mathematical Assistants: 14th Symposium, Calculemus 2007, 6th International Conference, MKM 2007, Hagenberg, Austria, June 27-30, 2007. Proceedings. Kauers, M., Kerber, M., Miner, R. & Windsteiger, W. (eds.). Springer Berlin Heidelberg, p. 161-175 15 p. (Lecture Notes in Computer Science; vol. 4573).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  • Datatypes in Memory

    Aspinall, D. & Hoffman, P., 2007, Proceedings of the 2nd International Conference on Algebra and Coalgebra in Computer Science. Berlin, Heidelberg: Springer-Verlag, p. 111-125 15 p. (CALCO'07).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  • Formalising Java’s Data Race Free Guarantee

    Aspinall, D. & Ševčík, J., 2007, Theorem Proving in Higher Order Logics: 20th International Conference, TPHOLs 2007, Kaiserslautern, Germany, September 10-13, 2007. Proceedings. Schneider, K. & Brandt, J. (eds.). Springer Berlin Heidelberg, p. 22-37 16 p. (Lecture Notes in Computer Science; vol. 4732).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  • Isabelle with Proof General Eclipse: An Overview and User Introduction

    Aspinall, D. & Lüth, C., 2007, CADE-21 The 21st Conference on Automated Deduction : The Isabelle Workshop 2007. p. 38 1 p.

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  • Java Memory Model Examples: Good, Bad and Ugly

    Aspinall, D. & Ševčík, J., 2007, Proceedings of Verification and Analysis of Multi-Threaded Java-Like Programs (VAMP 2007). 15 p.

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

    Open Access
    File
  • Mobile Resource Guarantees

    Sannella, D., Hofmann, M., Aspinall, D., Gilmore, S., Stark, I., Beringer, L., Loidl, H-W., MacKenzie, K., Momigliano, A. & Shkaravska, O., 2007, Trends in Functional Programming. Intellect Books, Vol. 6. p. 211-226 16 p.

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

    Open Access
    File
  • 2006

    Assisted Proof Document Authoring

    Aspinall, D., Lüth, C. & Wolff, B., 2006, Mathematical Knowledge Management: 4th International Conference, MKM 2005, Bremen, Germany, July 15-17, 2005, Revised Selected Papers. Kohlhase, M. (ed.). Springer Berlin Heidelberg, p. 65-80 16 p. (Lecture Notes in Computer Science; vol. 3863).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  • Mobile Resource Guarantees and Policies

    Aspinall, D. & MacKenzie, K., 2006, Mobile Resource Guarantees and Policies: Construction and Analysis of Safe, Secure, and Interoperable Smart Devices. Barthe, G., Grégoire, B., Huisman, M. & Lanet, J-L. (eds.). Springer Berlin Heidelberg, p. 16-36 21 p. (Lecture Notes in Computer Science; vol. 3956).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

    Open Access
    File
  • PG Tips: A Recommender System for an Interactive Theorem Prover

    Mercer, A. E., Bundy, A., Duncan, H. & Aspinall, D., 2006, Proceedings of Mathematical User-Interfaces Workshop (MathUI’2006). p. 1-8 8 p.

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

    Open Access
    File
  • Proof General in Eclipse: System and Architecture Overview

    Aspinall, D., Winterstein, D., Lüth, C. & Fayyaz, A., 2006, eclipse '06 Proceedings of the 2006 OOPSLA workshop on eclipse technology eXchange. New York, NY, USA: ACM, p. 45-49 5 p.

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  • 2005

    Mobile Resource Guarantees (Project Evaluation Paper)

    Sannella, D., Hofmann, M., Aspinall, D., Gilmore, S., Stark, I., Beringer, L., Loidl, H-W., MacKenzie, K., Momigliano, A. & Shkaravska, O., 2005, 6th Symposium on Trends in Functional Programming TFP 2005. Institute of Cybernetics, p. 7-16 10 p.

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  • Mobile Resource Guarantees for Smart Devices

    Aspinall, D., Gilmore, S., Hofmann, M., Sannella, D. & Stark, I., 2005, Construction and Analysis of Safe, Secure, and Interoperable Smart Devices: International Workshop, CASSIS 2004, Marseille, France, March 10-14, 2004, Revised Selected Papers. Barthe, G., Burdy, L., Huisman, M., Lanet, J-L. & Muntean, T. (eds.). Berlin: Springer-Verlag GmbH, Vol. 3362. p. 1-26 26 p. (Lecture Notes in Computer Science; vol. 3362).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

    Open Access
    File
  • Parsing, editing, proving: The PGIP display protocol

    Aspinall, D., Lüth, C. & Winterstein, D., 2005, International Workshop on User Interfaces for Theorem Provers. Vol. 2005.

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

    File
  • Proof General/Eclipse: A Generic Interface for Interactive Proof

    Aspinall, D., Lüth, C. & Winterstein, D., 2005, Proceedings of the 19th International Joint Conference on Artificial Intelligence. San Francisco, CA, USA: Morgan Kaufmann Publishers Inc., p. 1587-1588 2 p. (IJCAI'05).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

    Open Access
    File
  • 2004

    A Program Logic for Resource Verification

    Aspinall, D., Beringer, L., Hofmann, M., Loidl, H-W. & Momigliano, A., 2004, Theorem Proving in Higher Order Logics: 17th International Conference, TPHOLs 2004, Park City, Utah, USA, September 14-17, 2004. Proceedings. Slind, K., Bunker, A. & Gopalakrishnan, G. (eds.). Springer Berlin Heidelberg, Vol. 3223. p. 34-49 16 p. (Lecture Notes in Computer Science; vol. 3223).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  • 2002

    Another Type System for In-Place Update

    Aspinall, D. & Hofmann, M., 2002, Programming Languages and Systems: 11th European Symposium on Programming, ESOP 2002 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2002 Grenoble, France, April 8–12, 2002 Proceedings. Le Métayer, D. (ed.). Springer Berlin Heidelberg, Vol. 2305. p. 36-52 17 p. (Lecture Notes in Computer Science; vol. 2305).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  • From Specifications to Code in Casl

    Aspinall, D. & Sannella, D., 2002, Algebraic Methodology and Software Technology: 9th International Conference, AMAST 2002 Saint-Gilles-les-Bains, Reunion Island, France September 9–13, 2002 Proceedings. Kirchner, H. & Ringeissen, C. (eds.). Springer Berlin Heidelberg, Vol. 2422. p. 1-14 14 p. (Lecture Notes in Computer Science; vol. 2422).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  • Type Checking Parametrised Programs and Specifications in ASL+_FPC

    Aspinall, D., 2002, Recent Trends in Algebraic Development Techniques: 16th International Workshop, WADT 2002, Frauenchiemsee, Germany, September 24-27, 2002, Revised Selected Papers. Springer Berlin Heidelberg, p. 129-144 16 p. (Lecture Notes in Computer Science; vol. 2755).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  • 2000

    Protocols for Interactive e-Proof

    Aspinall, D., Jul 2000, Supplemental proceedings of the 13th international conference on theorem proving in higher order logics (TPHOLs 2000). p. 25-32 8 p.

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  • Proof General: A Generic Tool for Proof Development

    Aspinall, D., 2000, Tools and Algorithms for the Construction and Analysis of Systems: 6th International Conference, TACAS 2000 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2000 Berlin, Germany, March 25 – April 2, 2000 Proceedings. Graf, S. & Schwartzbach, M. (eds.). Springer Berlin Heidelberg, Vol. 1785. p. 38-43 6 p. (Lecture Notes in Computer Science; vol. 1785).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  • Subtyping with Power Types

    Aspinall, D., 2000, Computer Science Logic: 14th Annual Conference of the EACSL, Fischbachau, Germany, August 21-26, 2000, Proceedings. Springer Berlin Heidelberg, p. 156-171 16 p. (Lecture Notes in Computer Science; vol. 1862).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  • 1996

    Subtyping dependent types (Summary)

    Aspinall, D. & Compagnoni, A., 1996, LICS '96. Proceedings., Eleventh Annual IEEE Symposium on Logic in Computer Science, 1996. Institute of Electrical and Electronics Engineers (IEEE), p. 86-97 10 p.

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  • 1995

    Subtyping with singleton types

    Aspinall, D., 1995, Computer Science Logic: 8th Workshop, CSL '94 Kazimierz, Poland, September 25–30, 1994 Selected Papers. Pacholski, L. & Tiuryn, J. (eds.). Springer Berlin Heidelberg, Vol. 933. p. 1-15 15 p. (Lecture Notes in Computer Science; vol. 933).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  • Types, subtypes, and ASL+

    Aspinall, D., 1995, Recent Trends in Data Type Specification: 10th Workshop on Specification of Abstract Data Types Joint with the 5th COMPASS Workshop S. Margherita, Italy, May 30 – June 3, 1994 Selected Papers. Astesiano, E., Reggio, G. & Tarlecki, A. (eds.). Springer Berlin Heidelberg, Vol. 906. p. 116-131 16 p. (Lecture Notes in Computer Science; vol. 906).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution