Code-carrying
authorization
(With S. Maffeis, M. Abadi, and
C. Fournet.
ESORICS’08) [Details]
Type
inference for correspondence types
(With H. Huettel
and R. Rydhof Hansen.
SecCo’08) [Details]
Refinement
types for secure implementations
(With J. Bengtson, K.
Bhargavan, C. Fournet, and S. Maffeis. CSF’08) [Details]
Service
combinators for farming virtual machines
(With K. Bhargavan and I.
Narasamdya.
COORDINATION’08) [Details]
Getting
operations logic right: types, service-orientation, and static analysis
(With K. Bhargavan. Rise and Rise of the
Declarative Datacentre, 2008) [Details]
Rise
and Rise of the Declarative Datacentre
(Co-editor with K. Bhargavan, T. Harris, and P. Toft. MSR
TR-2008-61) [Details]
Verified
implementations of the Information Card federated identity-management protocol
(With K. Bhargavan, C.
Fournet, and N. Swamy.
ASIACCS’08) [Details]
A
chart
semantics for the pi-calculus
(With J. Borgstroem
and A. Phillips.
EXPRESS'07) [Details]
A
type system for authorization in distributed systems
(With C. Fournet and S.
Maffeis.
CSF’07) [Details]
Design
and semantics of a decentralised authorization language
(With M. Becker and C.
Fournet.
CSF’07) [Details]
Verified
reference implementations of WS-Security protocols
(With K. Bhargavan and C.
Fournet.
WSFM'06) [Details]
Provable
implementations of security protocols
(LICS'06) [Details]
Verified
interoperable implementations of security protocols
(With K. Bhargavan, C.
Fournet, and S. Tse.
CSFW'06) [Details]
Policy
Advisor for WSE 3
(With K. Bhargavan and C.
Fournet. WSE
Patterns and Guidance, 2006) [Details]
An
advisor for web services security policies
(With K. Bhargavan, C.
Fournet, and G. O'Shea.
SWS'05) [Details]
Algebraic
Process Calculi: The First Twenty Five Years and Beyond
(Co-editor with L. Aceto. BRICS Note NS-05-03) [Details]
Secrecy
despite compromise: types, cryptography, and the pi-calculus
(With A. Jeffrey. CONCUR'05) [Details]
Foundations
of Software Science and Computation Structures
(Editor. TCS Volume 333) [Details]
A
type discipline for authorization policies
(With C. Fournet and S.
Maffeis.
ESOP'05) [Details]
Secure
sessions for web services
(With K. Bhargavan, R. Corin,
and C. Fournet.
SWS'04) [Details]
Verifying
Policy-Based Security for Web Services
(With K. Bhargavan and C.
Fournet.
CCS'04) [Details]
TulaFale: A security tool for web services
(With K. Bhargavan, C. Fournet,
and R. Pucella.
FMCO'03) [Details]
From
stack inspection to access control: A security analysis for libraries
(With F. Besson,
T. Blanc, and C. Fournet. CSFW'04) [Details]
A
semantics for web services authentication
(With K. Bhargavan and C.
Fournet.
POPL'04) [Details]
Foundations
of Software Science and Computation Structures (FOSSACS 2003)
(Editor) [Details]
Deciding
validity in a spatial logic for trees
(With C. Calcagno and L.
Cardelli.
TLDI 2003) [Details]
Validating
a web service security abstraction by typing
(With R. Pucella. XML Security, 2002) [Details]
Typing
one-to-one and one-to-many correspondences in security protocols
(With A. Jeffrey. ISSS, 2002) [Details]
Automating
type soundness proofs via decision procedures and guided reductions
(With D. Syme. LPAR, 2002) [Details]
Types
and effects for asymmetric cryptographic protocols
(With A. Jeffrey. CSFW, 2002) [Details]
Finite-control
mobile ambients
(With W. Charatonik
and J.-M.
Talbot. ESOP'02) [Details]
Stack
inspection: theory and variants
(With C. Fournet. POPL'02) [Details]
Types
for the ambient calculus
(With L. Cardelli and G.
Ghelli.
Collation of material presented at POPL99, ICALP'99, and TCS 2000) [Details]
Notes
on nominal calculi for security and mobility
(FOSAD book, 2002) [Details]
Authenticity
by typing for security protocols
(With A. Jeffrey. CSFW, 2001) [Details]
Typing
correspondence assertions for communication protocols
(With A. Jeffrey. MFPS, 2001) [Details]
Logical
properties of name restriction
(With L. Cardelli. TLCA'01) [Details]
The
complexity of model checking mobile ambients
(With W. Charatonik,
S. Dal Zilio, S. Mukhopadhyay, and J.-M. Talbot. FOSSACS'01) [Details]
Typing
a multilanguage intermediate code
(With D. Syme. POPL'01) [Details]
A
commitment relation for the ambient calculus
(With L. Cardelli. Note, 2000) [Details]
Region
analysis and a p-calculus
with groups
(With S. Dal
Zilio. MFCS'00) [Details]
Secrecy
and group creation
(With L. Cardelli and G.
Ghelli.
CONCUR 2000) [Details]
Ambient
groups and mobility types
(With L. Cardelli and G.
Ghelli.
TCS2000) [Details]
Anytime,
anywhere: modal logics for mobile ambients
(With L. Cardelli. POPL'00) [Details]
Mobility
types for mobile ambients
(With L. Cardelli and G.
Ghelli.
ICALP'99) [Details]
Equational properties of mobile ambients
(With L. Cardelli. FOSSACS'99) [Details]
Types
for mobile ambients
(With L. Cardelli. POPL'99) [Details]
A
concurrent object calculus: reduction and typing
(With P. D. Hankin, HLCL'98) [Details]
A
bisimulation method for cryptographic protocols
(With M. Abadi. ESOP'98) [Details]
Mobile
ambients
(With L. Cardelli. FOSSACS'98) [Details]
A
calculus for cryptographic protocols: the spi calculus
(With M. Abadi. Information and Computation,
148:1-70 (1999)) [Details]
Operational
equivalences for untyped and polymorphic object
calculi
(HOOTS book, 1998) [Details]
Higher
Order Operational Techniques in Semantics
(Editor with Andrew M. Pitts. CUP, 1998) [Details]
Compilation
and equivalence of imperative objects
(With P. D. Hankin and S. B. Lassen. FST&TCS'97) [Details]
Reasoning
about cryptographic protocols in the spi calculus
(With M. Abadi. CONCUR'97) [Details]
A
calculus for cryptographic protocols: the spi calculus
(With M. Abadi. CCS'97) [Details]
Nominal
calculi for security and mobility
(FSMC'97) [Details]
Five
axioms of alpha-conversion
(With T.F. Melham. HUG'96) [Details]
The
Haskell language report, version 1.3
(With others. Yale, 1996) [Details] [HTML]
The
Haskell library report, version 1.3
(With others. Yale, 1996) [Details] [HTML]
Book
review
(JFP, 1996) [Details]
Concurrent
Haskell
(With S. Peyton Jones and S. Finne. POPL'96) [Details]
Bisimilarity
for a first-order calculus of objects with subtyping
(With G.D. Rees. POPL'96) [Details]
A
HOL embedding of a small parallel HDL.
(With M. Larson. HUG'95)
Monadic
I/O in Haskell 1.3.
(With K. Hammond. Haskell'95) [Details]
Bisimilarity
as a theory of functional programming.
(MFPS'95) [Details]
A
tutorial on co-induction and functional programming.
(Glasgow FP'94) [Details]
A
sound metalogical semantics for input/output effects.
(With R.L. Crole. CSL'94) [Details]
A
mechanisation of name-carrying syntax up to alpha-conversion.
(HUG'93) [Details]
Factoring
an adequacy proof (preliminary report).
(With R.L. Crole. Glasgow FP'93) [Details]
An
operational semantics for I/O in a lazy functional language.
(FPCA'93) [Details]
Example:
the binomial theorem.
(HOL book, CUP, 1993) [Details]
The
formal definition of a synchronous hardware-description language in higher
order logic.
(ICCD'92) [Details]
Experience
with embedding hardware description languages in HOL.
(With R. Boulton, M. Gordon, J.
Harrison, J. Herbert, J. Van Tassell.
TPCD'92) [Details]
Functional
Programming and Input/Output.
(PhD dissertation, Cambridge, 1992; CUP, 1994) [Details]