Selected publications by Luis Caires

Recent papers and drafts

Termination in Session-Based Concurrency via Linear Logical Relations (draft of a paper to appear at ESOP'12, with Jorge Perez, Frank Pfenning and Bernardo Toninho).

Functions as Session Typed Processes (draft of a paper to appear at FoSSaCS'12, with Frank Pfenning and Bernardo Toninho).

SLMC: A Tool for Model Checking Concurrent Systems against Dynamical Spatial Logic Specifications (draft of a paper to appear at TACAS'12, with Hugo T. Vieira).

Towards Concurrent Type Theory (draft of a paper to appear at TLDI'12, with Frank Pfenning and Bernardo Toninho).

Dynamic Roles in Multiparty Communicating Systems (draft, with Pedro Baltazar, Vasco T. Vasconcelos, and Hugo T. Vieira).

Analysing Service based Software Systems with the Conversation Calculus to appear in FACS'10 post proceedings (with Hugo Vieira).

Proof-Carrying Code in a Session-Typed Process Calculus in CPP'11 (with Frank Pfenning and Bernardo Toninho).

Dependent Session Types via Intuitionistic Linear Type Theory in PPDP'11 (with Bernardo Toninho and Frank Pfenning).

Type Based Access Control for Data Centric Applications in ESOP'11 (with Jorge A. Perez, Joao C. Seco, Hugo T. Vieira, and Lucio Ferrao).

Session Types as Intuitionistic Linear Propositions in CONCUR'10 (with Frank Pfenning).

Aliasing Control with View-based Typestate in Formal Techniques for Java Programs FTfJP'10, 2010 (with Filipe Militao and Jonathan Aldrich).

Core Calculi for Service-Oriented Computing (with Rocco De Nicola, Rosario Pugliese, Vasco T. Vasconcelos and Gianluigi Zavattaro).

Tools and Verification (with Massimo Bartoletti, Ivan Lanese, Franco Mazzanti, Davide Sangiorgi, Hugo Torres Vieira and Roberto Zunino).

A Spatial-Epistemic Logic for Reasoning about Security Protocols in SecCo'10 (with Bernardo Toninho).

A Type System for Access Control Views in Object-Oriented Languages in ARSPA-WITS'10 (with Mário Pires).

Type Inference for Conversation Types in PLACES'10 (with Luisa Lourenço).

Conversation Types to appear in Theoretical Computer Science, 2010 (with Hugo T. Vieira).

Spatial-Behavioral Types for Concurrency and Resource Control in Distributed Systems in Theoretical Computer Science 402(2-3), 2008.

Dynamic Spatial Logics: A Tutorial Survey in Bulletin of the EATCS 94, 2008.

by topic

Concurrency models and logics

A Process Calculus Analysis of Compensations.

Luis Caires, Carla Ferreira and Hugo T. Vieira.
To appear in TGC'08 Proceedings (Springer-Verlag, Lecture Notes in Computer Science), 2008.
Preprint available in pdf format.

Logical Semantics of Types for Concurrency

Luís Caires.
In CALCO'07 Proceedings (Springer-Verlag, Lecture Notes in Computer Science), 2007.
Preprint available in pdf format.

Extensionality of Spatial Observations in Distributed Systems

Luís Caires and Hugo T. Vieira.
In EXPRESS'2006 Proceedings (EN in Theoretical Computer Science), 2006.
Preprint available in pdf format. Full version with proofs here.

Elimination of Quantifiers and Undecidability in Spatial Logics for Concurrency

Luís Caires and Etiénne Lozes.
Theoretical Computer Science, Vol 358/2, 2006, Elsevier.
Preprint available in compressed postscript format.

Elimination of Quantifiers and Undecidability in Spatial Logics for Concurrency

Luís Caires and Etiénne Lozes.
Appears in CONCUR'2004 Proceedings, #3170 of Lecture Notes in Computer Science, Springer-Verlag, 2004
Preprint available in compressed postscript format.

Behavioral and Spatial Observations in a Logic for the Pi-Calculus

Luís Caires.
Appears in ETAPS.FOSSACS'2004 Proceedings, #2987 of Lecture Notes in Computer Science, Springer-Verlag, 2004.
Preprint available in compressed postscript format.

A Spatial Logic for Concurrency (Part II)

Luís Caires and Luca Cardelli.
Appears in Theoretical Computer Science, Vol 322/3, 2004, Elsevier.
Preprint available in compressed postscript format.

A Spatial Logic for Concurrency (Part II)

Luís Caires and Luca Cardelli.
Appears in CONCUR'2002 Proceedings, #2421 of Lecture Notes in Computer Science, Springer-Verlag, 2002.
Available in compressed postscript format.

A Spatial Logic for Concurrency (Part I)

Luís Caires and Luca Cardelli.
Appears in Journal of Information and Computation 186(2), 2003, Elsevier.
Preprint available in compressed postscript format.

A Spatial Logic for Concurrency (Part I)

Luís Caires and Luca Cardelli.
Appears in TACS 2001 Proceedings, Lecture Notes in Computer Science, Springer-Verlag, 2001.
Available in compressed postscript format

A Specification Logic for Mobility

Luís Caires.
DI/FCT/UNL Technical Report 4/2000.
Available in compressed postscript format.

A Model for Declarative Programming and Specification with Concurrency and Mobility PhD Thesis

Specifying Dynamic Object Systems

Luís Caires and Luís Monteiro.
DI/FCT/UNL Technical Report 10/98.
Available in compressed postscript format.
(superseded by "A Specification Logic for Mobility" above).

Verifiable and Executable Logic Specifications of Concurrent Objects in Lpi

Luís Caires and Luís Monteiro.
Appeareds in the ETAPS/ESOP98 proceedings. #1381 of Lecture Notes in Computer Science, Springer-Verlag 1998.
Available in compressed postscript format.

Lpi encodings of choices, exceptions and first-class events

Luís Caires.
DI/FCT/UNL Technical Report 8/98.
Available in compressed postscript format.

Proof Net Semantics of Proof Search Computation

Luís Caires and Luís Monteiro.
Appeared in the ALP'97 proceedings. #1298 of Lecture Notes in Computer Science, Springer-Verlag 1997.
Available in compressed postscript format.

A Language for the Logical Specification of Processes and Relations

Luís Caires and Luís Monteiro.
Appeared in the ALP'96 proceedings. #1139 of Lecture Notes in Computer Science, Springer-Verlag 1996.
Available in compressed postscript format.

A Language for Executable Logical Specification of Processes and Relations

Luís Caires.
DI/FCT/UNL Technical Report 6/96.
Extended version of paper above.
Available in compressed postscript format (173403 bytes).

Programming Languages and Types

Conversation Types

Luis Caires and Hugo T. Vieira.
in ESOP'09 Proceedings (Springer-Verlag, Lecture Notes in Computer Science).
Preprint available in pdf format.
Long version with proofs: DI/FCT/UNL Technical Report 3/08

Spatial-Behavioral Types for Concurrency and Resource Control in Distributed Systems

Luís Caires. In Theoretical Computer Science 402(2-3), 2008. Preprint

The Conversation Calculus: A Model of Service Oriented Computation

Hugo T. Vieira, Luis Caires and João C. Seco.
in ESOP'2008 Proceedings (Springer-Verlag, Lecture Notes in Computer Science).
Preprint available in pdf format.
Long Version with proofs (TR DIFCTUNL 6/07).

Spatial-Behavioral Types, Distributed Services, and Resources

Luís Caires.
In TGC'2006 Proceedings (Springer-Verlag, Lecture Notes in Computer Science).
Preprint available in pdf format.

Types for Dynamic Reconfiguration

João Seco and Luís Caires.
To appear in ESOP'2006 Proceedings. Lecture Notes in Computer Science, Springer Verlag, 2006.
Preprint availaible in pdf format.

Subtyping First-Class Polymorphic Components

João Seco and Luís Caires.
ESOP'2005 Proceedings. #3444 of Lecture Notes in Computer Science, Springer Verlag, 2005.
Preprint availaible in pdf format.

A Basic Model of Typed Components

João Seco and Luís Caires.
Appeared in ECOOP'2000 Proceedings. #1850 of Lecture Notes in Computer Science, Springer-Verlag 2000.
Available in compressed postscript format.

A Basic Model of Typed Components

João Seco and Luís Caires.
Extended Version of the ECOOP'2000 paper above. DI/FCT/UNL Technical Report 1/2000.
Available in compressed postscript format.

Parametric Typed Components

Joăo Seco and Luís Caires.
WCOP'2000 Proceedings.
Available in compressed postscript format.

Logic programming and Unification

Unificação de Ordem Superior Polimórfica para a Programação em Lógica
Master Thesis, February 1995

Higher-Order Polymorphic Unification for Logic Programming

Luís Caires and Luís Monteiro.
Appeared in ICLP'94 Proceedings, MIT Press, 1994.

SLWV - A Theorem Prover for Logic Programming

Luis Moniz Pereira, Luís Caires and José Alferes.
Appeared in ELP'92 Proceedings. #660 of Lecture Notes in Artificial Intelligence 660, Spriger-Verlag.

Classical Negation in Logic Programs

Luis Moniz Pereira, Luís Caires and José Alferes.
Appeared in the Proceedings of the Brazilian Symposium of Artificial Inteligence, 1990.

Towards Distributed Tools for Heterogeneous Logic Programming Environments

José Alegria and Artur Dias and Luís Caires.
Appeared in ICLP'90 Proceedings, MIT Press, 1990.