Selected publications by Luis Caires

Recent Papers and Drafts

Propositions-as-Types and Shared State (ICFP 2021, to appear) (with Pedro Rocha)

Propositions-as-Types and Shared State (NOVA LINCS Tech Report 10/2021) (with Pedro Rocha)

Domain-Aware Session Types CONCUR'19 (with Jorge Perez, Frank Pfenning, Bernardo Toninho).

Refinement Kinds OOPSLA'19 (with Bernardo Toninho).

Linearity, Control Effects, and Behavioral Types ESOP'17 (with Jorge Perez).

Foundations of Session Types and Behavioural Contracts ACM Comp. Surv. 2016 (Huttel et al.).

Linear logic propositions as session types Math. Struct. Comp. Sci. 2016 (with Toninho and Pfenning).

Composing Interfering Abstract Protocols ECOOP'16 (with Aldrich and Militao).

Multiparty Session Types Within a Canonical Binary Theory, and Beyond. FORTE'16 (with Perez).

Dependent Information Flow Types POPL'15 (with Luisa Lourenço). DIFT Type Checker Prototype.

Linear Logical Relations and Observational Equivalences for Session-Based Concurrency in Information and Computation, 2014 (with J. Perez, F. Pfenning, and B. Toninho).

Co-recursion in Session-Typed Processes in TGC'14 (with Bernardo Toninho and Frank Pfenning).

Rely-Guarantee Protocols in ECOOP'14 (with Filipe Militão and Jonathan Aldrich).

Substructural Typestates in PLPV'14 (with Filipe Militão and Jonathan Aldrich).

Relating Multiparty and Binary Session Types via Linear Logic draft (with Jorge A. Perez).

Logic-Based Domain-Aware Session Types draft (with Bernardo Toninho, Jorge A. Perez and Frank Pfenning).

The Type Discipline of Behavioral Separation in POPL'13 (with Joao C. Seco).

Working note on a type-checking algorithm for BST, with checked examples (from paper above).

Higher-Order Processes, Functions, and Sessions: A Monadic Integration in ESOP'13 (with Bernardo Toninho and Frank Pfenning).

Behavioral Polymorphism and Parametricity in Session-Based Communication in ESOP'13 (with Jorge A. Perez, Frank Pfenning, and Bernardo Toninho).

Value Dependent Information Flow Analysis for Data Security in TGC'13 (with Luísa Lourenço).

Cut Reduction in Linear Logic as Asynchronous Session-Typed Communication in CSL'12 (with Henry DeYoung, Frank Pfenning and Bernardo Toninho).

A Type System for Flexible Role Assignment in Multiparty Communicating Systems in TGC'12 (with Pedro Baltazar, Vasco T. Vasconcelos, and Hugo T. Vieira).

Linear Logical Relations for Session-Based Concurrency in ESOP'12 (with Jorge Perez, Frank Pfenning and Bernardo Toninho).

Functions as Session Typed Processes in FoSSaCS'12 (with Frank Pfenning and Bernardo Toninho).

SLMC: A Tool for Model Checking Concurrent Systems against Dynamical Spatial Logic Specifications in TACAS'12 (with Hugo T. Vieira).

Towards Concurrent Type Theory in TLDI'12 (with Frank Pfenning and Bernardo Toninho).

Analysing Service based Software Systems with the Conversation Calculus in FACS'10 (with Hugo T. 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 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.

Pre 2008 - by topic

Concurrency models and logics

A Process Calculus Analysis of Compensations.

Luis Caires, Carla Ferreira and Hugo T. Vieira.
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.