David Aspinall

Proceedings of the Intelligent Computer Mathematics, 2013

Polar: A Framework for Proof Refactoring.

[BibT_eX]

[DOI]

Dominik Dietrich

Iain Whiteside

Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2013

A Semantic Basis for Proof Queries and Transformations.

[BibT_eX]

[DOI]

Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2013

"Give Me Letters 2, 3 and 6!": Partial Password Implementations and Attacks.

[BibT_eX]

[DOI]

Mike Just

Proceedings of the Financial Cryptography and Data Security, 2013

2012

Querying Proofs.

[BibT_eX]

[DOI]

Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2012

On the security and usability of dual credential authentication in UK online banking.

[BibT_eX]

[DOI]

Mike Just

Proceedings of the 7th International Conference for Internet Technology and Secured Transactions, 2012

An Essence of SSReflect.

[BibT_eX]

[DOI]

Iain Whiteside

Gudmund Grov

Proceedings of the Intelligent Computer Mathematics - 11th International Conference, 2012

2011

Towards Formal Proof Script Refactoring.

[BibT_eX]

[DOI]

Proceedings of the Intelligent Computer Mathematics - 18th Symposium, 2011

Probing Attacks on Multi-Agent Systems Using Electronic Institutions.

[BibT_eX]

[DOI]

Shahriar Bijani

David Robertson

Proceedings of the Declarative Agent Languages and Technologies IX, 2011

2010

Tactics for Hierarchical Proof.

[BibT_eX]

[DOI]

Math. Comput. Sci., 2010

Preface.

[BibT_eX]

[DOI]

Claudio Sacerdoti Coen

Proceedings of the 9th International Workshop On User Interfaces for Theorem Provers, 2010

Symbolic and Analytic Techniques for Resource Analysis of Java Bytecode.

[BibT_eX]

[DOI]

Proceedings of the Trustworthly Global Computing - 5th International Symposium, 2010

2009

Personal choice and challenge questions: a security and usability assessment.

[BibT_eX]

[DOI]

Mike Just

Proceedings of the 5th Symposium on Usable Privacy and Security, 2009

Towards a Type System for Security APIs.

[BibT_eX]

[DOI]

Gavin Keighren

Graham Steel

Proceedings of the Foundations and Applications of Security Analysis, 2009

2008

A type system with usage aspects.

[BibT_eX]

[DOI]

Martin Hofmann

Michal Konecný

J. Funct. Program., 2008

Towards Merging PlatOmega and PGIP.

[BibT_eX]

[DOI]

Proceedings of the 8th International Workshop on User Interfaces for Theorem Provers, 2008

On Validity of Program Transformations in the Java Memory Model.

[BibT_eX]

[DOI]

Jaroslav Sevcík

Proceedings of the ECOOP 2008, 2008

A Tactic Language for Hiproofs.

[BibT_eX]

[DOI]

Proceedings of the Intelligent Computer Mathematics, 9th International Conference, 2008

2007

A program logic for resources.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 2007

Special Issue on User Interfaces in Theorem Proving: Preface.

[BibT_eX]

[DOI]

J. Autom. Reason., 2007

Monitoring External Resources in Java MIDP.

[BibT_eX]

[DOI]

Patrick Maier

Ian Stark

Proceedings of the First International Workshop on Run Time Enforcement for Mobile and Distributed Systems, 2007

Formalising Java's Data Race Free Guarantee.

[BibT_eX]

[DOI]

Jaroslav Sevcík

Proceedings of the Theorem Proving in Higher Order Logics, 20th International Conference, 2007

A Framework for Interactive Proof.

[BibT_eX]

[DOI]

Daniel Winterstein

Proceedings of the Towards Mechanized Mathematical Assistants, 14th Symposium, 2007

Safety Guarantees from Explicit Resource Management.

[BibT_eX]

[DOI]

Patrick Maier

Ian Stark

Proceedings of the Formal Methods for Components and Objects, 6th International Symposium, 2007

Datatypes in Memory.

[BibT_eX]

[DOI]

Piotr Hoffman

Proceedings of the Algebra and Coalgebra in Computer Science, 2007

2006

Optimisation Validation.

[BibT_eX]

[DOI]

Lennart Beringer

Alberto Momigliano

Proceedings of the 5th International Workshop on Compiler Optimization meets Compiler Verification, 2006

Proof general in Eclipse: system and architecture overview.

[BibT_eX]

[DOI]

Proceedings of the 2006 OOPSLA workshop on Eclipse Technology eXchange, 2006

2005

Mobile Resource Guarantees (project evaluation paper).

[BibT_eX]

Proceedings of the Revised Selected Papers from the Sixth Symposium on Trends in Functional Programming, 2005

Assisted Proof Document Authoring.

[BibT_eX]

[DOI]

Burkhart Wolff

Proceedings of the Mathematical Knowledge Management, 4th International Conference, 2005

Proof General / Eclipse: A Generic Interface for Interactive Proof.

[BibT_eX]

[DOI]

Daniel Winterstein

Proceedings of the IJCAI-05, Proceedings of the Nineteenth International Joint Conference on Artificial Intelligence, Edinburgh, Scotland, UK, July 30, 2005

Mobile Resource Guarantees and Policies.

[BibT_eX]

[DOI]

Kenneth MacKenzie

Proceedings of the Construction and Analysis of Safe, 2005

2004

A Program Logic for Resource Verification.

[BibT_eX]

[DOI]

Proceedings of the Theorem Proving in Higher Order Logics, 17th International Conference, 2004

Mobile Resource Guarantees for Smart Devices.

[BibT_eX]

[DOI]

Proceedings of the Construction and Analysis of Safe, 2004

2003

Heap-Bounded Assembly Language.

[BibT_eX]

[DOI]

Adriana B. Compagnoni

J. Autom. Reason., 2003

Proof General meets IsaWin: Combining Text-Based And Graphical User Interfaces.

[BibT_eX]

[DOI]

Proceedings of the User Interfaces for Theorem Provers Workshop, 2003

Preface.

[BibT_eX]

[DOI]

Proceedings of the User Interfaces for Theorem Provers Workshop, 2003

2002

Type Checking Parametrised Programs and Specifications in ASL+<sub>FPC</sub>.

[BibT_eX]

[DOI]

Proceedings of the Recent Trends in Algebraic Development Techniques, 2002

Another Type System for In-Place Update.

[BibT_eX]

[DOI]

Martin Hofmann

Proceedings of the Programming Languages and Systems, 2002

From Specifications to Code in CASL.

[BibT_eX]

[DOI]

Donald Sannella

Proceedings of the Algebraic Methodology and Software Technology, 2002

2001

Subtyping dependent types.

[BibT_eX]

[DOI]

Adriana B. Compagnoni

Theor. Comput. Sci., 2001

2000

Proof General: A Generic Tool for Proof Development.

[BibT_eX]

[DOI]

Proceedings of the Tools and Algorithms for Construction and Analysis of Systems, 2000

Subtyping with Power Types.

[BibT_eX]

[DOI]

Proceedings of the Computer Science Logic, 2000

1997

Type systems for modular programs and specifications.

[BibT_eX]

[DOI]

PhD thesis, 1997

1996

Subtyping Dependent Types (Summary).

[BibT_eX]

[DOI]

Adriana B. Compagnoni

Proceedings of the Proceedings, 1996

1994

Subtyping with Singleton Types.

[BibT_eX]

[DOI]

Proceedings of the Computer Science Logic, 8th International Workshop, 1994

Types, Subtypes, and ASL+.

[BibT_eX]

[DOI]