Selected Publications by Eike Ritter
M. Koleini, E. Ritter and M. Ryan.
Model checking agent knowledge in dynamic access control policies
. In Proceedings of 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2013), March 2013.
M. Arapinis, L. Mancini, E. Ritter, M. Ryan, N. Golde, K. Redon, and R. Borgaonkar.
New privacy issues in mobile telephony: Fix and verification.
In Proceedings of 19th ACM Conference on Computer and Communications Security (CCS 2012)}, 2012.
Rehana Yasmin, Eike Ritter, Guilin Wang:
An Authentication Framework for Wireless Sensor Networks Using Identity-Based Signatures: Implementation and Evaluation.
IEICE Transactions 95-D(1): 126-133 (2012).
Matt Smart, Eike Ritter:
True Trustworthy Elections: Remote Electronic Voting Using Trusted Computing.
ATC 2011: 187-202.
Myrto Arapinis, Eike Ritter, Mark Dermot Ryan:
StatVerif: Verification of Stateful Processes.
CSF 2011: 33-47.
Rehana Yasmin, Eike Ritter, Guilin Wang:
An Authentication Framework for Wireless Sensor Networks using Identity-Based Signatures.
CIT 2010: 882-889
Myrto Arapinis, Tom Chothia, Eike Ritter, Mark Ryan:
Analysing Unlinkability and Anonymity Using the Applied Pi Calculus.
CSF 2010: 107-121.
Matt Smart, Eike Ritter:
Remote Electronic Voting with Revocable Anonymity.
ICISS 2009: 39-54.
V. de Paiva and E. Ritter.
A Parigot-style linear lambda-calculus for full intuitionistic linear logic.
Theory and Applications of Categories. Vol. 17, pp. 30-48, 2006.
M.E. Maietti, P. Maneggia, V. de Paiva, and E. Ritter.
Relating Categorical Semantics for Intuitionistic Linear Logic.
Applied Categorical Structures, vol 13, pp. 1-36, 2005.
S. Kremer, A. Mukhamedov and E. Ritter.
Analysis of a multi-party fair exchange protocol and formal proof of correctness in the strand space model.
Financial Cryptography'05 , LNCS 3570, pp. 255-269, 2005.
D. Pym and E. Ritter.
A games semantics for reductive logic and proof-search.
ETAPS'05-workshop on Games for Logic and Programming Languages, pp. 107-123, 2005.
M.E. Maietti, V. de Paiva and E. Ritter.
Normalization bounds in rudimentary linear logic
. Technical Report, University of Padova, June 2002.
N. Alechina, M. Mender, V. de Paiva and E. Ritter.
Categorical and Kripke Semantics for Constructive S4 Modal Logic
. CSL'01, LNCS 2142.
On the Semantics of Classical Disjunction (joint with David Pym). Journal of Pure and Applied Algebra 159, pp. 315-338, 2001.
dvi
ps
A calculus for Resource allocation.
Technical Report, University of Birmingham, October 2000.
Categorical Models for Intuitionistic and Linear Type Theory (Joint work with Maria Emilia Maietti and Valeria de Paiva). In Proc. of FoSSaCS'00. Lecture Notes of Computer Science 1784, pages 223--237.
dvi
.
ps
.
Characterising explicit substitutions which preserve termination.
In Proc. of TLCA'99. Lecture Notes in Computer Science 1561, pp. 325-339.
Explicit Substitutions for Linear Logical Frameworks (Joint work with Iliano Cervesato and Valeria de Paiva). In Proc. of the Workshop on Logical Frameworks and Meta-Languages (LFM'99).
ps
.
Categorical Models for Explicit Substitutions (joint with Neil Ghani and Valeria de Paiva). In Proc. of FoSSaCS'99. Lecture Notes in Computer Science 1578, pages 197--211.
dvi
ps
Explicit Substitutions for Constructive Necessity (joint with Neil Ghani and Valeria de Paiva). Presented at ICALP'98.
dvi
ps
Linear Explicit Substitutions (Joint work with Neil Ghani and Valeria de Paiva). Presented at Westapp'98.
dvi
ps
. The journal version appeared in the Journal of the IGPL, Vol, 8(1), pp.7-31.
Technical Report CSR-98-02
.
On Explicit Substitution and Names (joint with Valeria de Paiva). Presented at ICALP'97.
dvi
ps
On Explicit Substitution and Names (joint with Valeria de Paiva).
Technical Report, 1997.
Proof terms for classical and intuitionistic resolution (joint with David Pym and Lincoln Wallen). Presented at CADE'96.
dvi
ps
. Journal version published in Journal of Logic and Computation, 10(2), pp. 173--207, 2000.
dvi
ps
.
On the intuitionistic force of classical search (joint with David Pym and Lincoln Wallen). Presented at Tableaux'96.
dvi
ps
Journal version published in TCS 232(1-2), pp.299-333.
dvi
ps
A Fully Abstract Translation between a $\zl$-Calculus with Reference Types and Standard ML (joint paper with Andrew M. Pitts), presented at TLCA'95.
dvi
ps
Rewriting Properties of Combinators for Intuitionstic Linear Logic'' (joint with Monica Nesi and Valeria de Paiva) presented at HOA'93.
dvi
ps
Normalization for Typed Lambda Calculi with Explicit Substitution, presented at CSL'93.
dvi
ps
A Generic Strong Normalization Argument: Application to the Calculus of Constructions (joint with Luke Ong), presented at CSL'93.
dvi
ps
Categorical abstract machines for higher-order typed lambda calculi. Published in TCS.
dvi
ps
Categorical abstract machines for higher-order typed lambda calculi. PhD Thesis, University of Cambridge.
dvi
ps
Preprints
A
BibTeX database
is also available.
Page maintained by
E.Ritter@cs.bham.ac.uk