Selected Publications by Eike Ritter
V. de Paiva and E. Ritter.
A Parigot-style linear lambda-calculus for full intuitionistic linear logic.
Theory and Applications of Categories. Accepted for publication.
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
