Sciweavers

Share
TPHOL
2009
IEEE
10 years 4 months ago
Packaging Mathematical Structures
François Garillot, Georges Gonthier, Assia ...
TPHOL
2009
IEEE
10 years 4 months ago
A Formalisation of Smallfoot in HOL
In this paper a general framework for separation logic inside the HOL theorem prover is presented. This framework is based on Abeparation Logic. It contains a model of an abstract,...
Thomas Tuerk
TPHOL
2009
IEEE
10 years 4 months ago
A Better x86 Memory Model: x86-TSO
Abstract. Real multiprocessors do not provide the sequentially consistent memory that is assumed by most work on semantics and verification. Instead, they have relaxed memory mode...
Scott Owens, Susmit Sarkar, Peter Sewell
TPHOL
2009
IEEE
10 years 4 months ago
Formalising Observer Theory for Environment-Sensitive Bisimulation
Abstract. We consider a formalisation of a notion of observer (or intruder) theories, commonly used in symbolic analysis of security protocols. An observer theory describes the kno...
Jeremy E. Dawson, Alwen Tiu
TPHOL
2009
IEEE
10 years 4 months ago
The HOL-Omega Logic
A new logic is posited for the widely used HOL theorem prover, as an extension of the existing higher order logic of the HOL4 system. The logic is extended to three levels, adding ...
Peter V. Homeier
TPHOL
2009
IEEE
10 years 4 months ago
Practical Tactics for Separation Logic
Abstract. We present a comprehensive set of tactics that make it practical to use separation logic in a proof assistant. These tactics enable the verification of partial correctne...
Andrew McCreight
TPHOL
2009
IEEE
10 years 4 months ago
Psi-calculi in Isabelle
Psi-calculi are extensions of the pi-calculus, accommodating arbitrary nominal datatypes to represent not only data but also communication channels, assertions and conditions, givi...
Jesper Bengtson, Joachim Parrow
TPHOL
2009
IEEE
10 years 4 months ago
A Brief Overview of Agda - A Functional Language with Dependent Types
Abstract. We give an overview of Agda, the latest in a series of dependently typed programming languages developed in Gothenburg. Agda is based on Martin-L¨of’s intuitionistic t...
Ana Bove, Peter Dybjer, Ulf Norell
TPHOL
2009
IEEE
10 years 4 months ago
A Hoare Logic for the State Monad
Abstract. This pearl examines how to verify functional programs written using the state monad. It uses Coq’s Program framework to provide strong specifications for the standard ...
Wouter Swierstra
TPHOL
2009
IEEE
10 years 4 months ago
Let's Get Physical: Models and Methods for Real-World Security Protocols
Traditional security protocols are mainly concerned with key establishment and principal authentication and rely on predistributed keys and properties of cryptographic operators. I...
David A. Basin, Srdjan Capkun, Patrick Schaller, B...
books