Luís Caires

chapter

A Spatial Logic for Concurrency (Part I)

Luís Caires, Luca Cardelli

Lecture Notes in Computer Science > Theoretical Aspects of Computer Software > Invited Talk 1 > 1-37

We present a logic that can express properties of freshness, secrecy, structure, and behavior of concurrent systems. In addition to standard logical and temporal operators, our logic includes spatial operations corresponding to composition, local name restriction, and a primitive freshname quantifier. Properties can also be defined by recursion; a central theme of this paper is then the combination...

chapter

A Basic Model of Typed Components

João Costa Seco, Luís Caires

Lecture Notes in Computer Science > ECOOP 2000 — Object-Oriented Programming > Type Theory > 108-128

This paper studies specific language level abstractions for component-based programming. We propose a simple model which captures some basic ingredients—like explicit context dependence, dynamic binding and subtype polymorphism, late (dynamic) composition, and avoidance of inheritance in favor of object composition - that several authors have defended to be central to black-box object-oriented component...

book

CONCUR 2007 – Concurrency Theory

Luís Caires, Vasco T. Vasconcelos

Lecture Notes in Computer Science

chapter

Tools and Verification

Massimo Bartoletti, Luis Caires, Ivan Lanese, Franco Mazzanti, more

Lecture Notes in Computer Science > Rigorous Software Engineering for Service-Oriented Systems > Qualitative Analysis Techniques for Service-Oriented Computing > 408-427

This chapter presents different tools that have been developed inside the Sensoria project. Sensoria studied qualitative analysis techniques for verifying properties of service implementations with respect to their formal specifications. The tools presented in this chapter have been developed to carry out the analysis in an automated, or semi-automated, way. We present four different tools,...

chapter

Conversation Types

Luís Caires, Hugo Torres Vieira

Lecture Notes in Computer Science > Programming Languages and Systems > Service-Oriented Computing > 285-300

We present a type theory for analyzing concurrent multiparty interactions as found in service-oriented computing. Our theory introduces a novel and flexible type structure, able to uniformly describe both the internal and the interface behavior of systems, referred respectively as choreographies and contracts in web-services terminology. The notion of conversation builds on the fundamental concept...

chapter

The Conversation Calculus: A Model of Service-Oriented Computation

Hugo T. Vieira, Luís Caires, João C. Seco

Lecture Notes in Computer Science > Programming Languages and Systems > Concurrency > 269-283

We present a process-calculus model for expressing and analyzing service-based systems. Our approach addresses central features of the service-oriented computational model such as distribution, process delegation, communication and context sensitiveness, and loose coupling. Distinguishing aspects of our model are the notion of conversation context, the adoption of a context sensitive, message-passing-based...

chapter

Proof net semantics of proof search computation

Luís Caires, Luís Monteiro

Lecture Notes in Computer Science > Algebraic and Logic Programming > 194-208

We present a sound and complete compositional semantics, structured around certain abstractions of proof nets, for proof-search computation in a linear logic-based language. The model captures the interaction of agents in terms of the actions they engage into and of the dynamic creation of names. The model is adequate for reasoning about a notion of operational equivalence. We will also suggest how...

chapter

Type-Based Access Control in Data-Centric Systems

Luís Caires, Jorge A. Pérez, João Costa Seco, Hugo Torres Vieira, more

Lecture Notes in Computer Science > Programming Languages and Systems > 136-155

Data-centric multi-user systems, such as web applications, require flexible yet fine-grained data security mechanisms. Such mechanisms are usually enforced by a specially crafted security layer, which adds extra complexity and often leads to error prone coding, easily causing severe security breaches. In this paper, we introduce a programming language approach for enforcing access control policies...

chapter

Verifiable and executable logic specifications of concurrent objects in $$\mathcal{L}_\pi$$

Luís Caires, Luís Monteiro

Lecture Notes in Computer Science > Programming Languages and Systems > 42-56

We present the core- $$\mathcal{L}_\pi$$ fragment of $$\mathcal{L}_\pi$$ and its program logic. We illustrate the adequacy of $$\mathcal{L}_\pi$$ as a meta-language for jointly defining operational semantics and program logics of languages with concurrent and logic features, considering the case of a specification logic for concurrent objects addressing mobile features like creation...

chapter

A language for the logical specification of processes and relations

Luís Caires

Lecture Notes in Computer Science > Algebraic and Logic Programming > 150-164

Due to its ability to handle resources in a finely controlled way, linear logic is being adopted as a foundation of several logic programming and specification languages in which some notions of state can be modelled. In particular, some of these were proposed with the main motivation of allowing the specification of concurrent systems: such systems incorporate small subsets of linear logic or have...

chapter

SLWV — A theorem prover for logic programming

Luís Moniz Pereira, Luis Caires, José Alferes

Lecture Notes in Computer Science > Extensions of Logic Programming > 1-23

The purpose of this work is to define a theorem prover that retains the procedural aspects of logic programing. The proof system we propose (SLWV-resolution. for Selected Linear Without contrapositive clause Variants)) is defined for a set of clauses in the implicational form (keeping to the form of logic programs). not requiring contrapositives, and has an execution method that respects the execution...

chapter

Proof-Carrying Code in a Session-Typed Process Calculus

Frank Pfenning, Luis Caires, Bernardo Toninho

Lecture Notes in Computer Science > Certified Programs and Proofs > Session 1: Logic and Types > 21-36

Dependent session types allow us to describe not only properties of the I/O behavior of processes but also of the exchanged data. In this paper we show how to exploit dependent session types to express proof-carrying communication. We further introduce two modal operators into the type theory to provide detailed control about how much information is communicated: one based on traditional proof irrelevance...

chapter

Spatial-Behavioral Types, Distributed Services, and Resources

Luís Caires

Lecture Notes in Computer Science > Trustworthy Global Computing > Types to Discipline Interactions > 98-115

We develop a notion of spatial-behavioral typing suitable to discipline interactions in service-based systems modeled in a distributed object calculus. Our type structure reflects a resource aware model of behavior, where a parallel composition type operator expresses resource independence, a sequential composition type operator expresses implicit synchronization, and a modal operator expresses resource...

chapter

Subtyping First-Class Polymorphic Components

João Costa Seco, Luís Caires

Lecture Notes in Computer Science > Programming Languages and Systems > 342-356

We present a statically typed, class-based object oriented language where classes are first class polymorphic values. A main contribution of this work is the design of a type system that combines first class polymorphic values with structural equirecursive types and admits a subtyping algorithm which is arguably much simpler than existing alternatives. Our development is modular and can be easily...

chapter

Session Types as Intuitionistic Linear Propositions

Luís Caires, Frank Pfenning

Lecture Notes in Computer Science > CONCUR 2010 - Concurrency Theory > 222-236

Several type disciplines for π-calculi have been proposed in which linearity plays a key role, even if their precise relationship with pure linear logic is still not well understood. In this paper, we introduce a type system for the π-calculus that exactly corresponds to the standard sequent calculus proof system for dual intuitionistic linear logic. Our type system is based on a new interpretation...

chapter

A Type System for Access Control Views in Object-Oriented Languages

Mário Pires, Luís Caires

Lecture Notes in Computer Science > Automated Reasoning for Security Protocol Analysis and Issues in the Theory of Security > 59-76

Access control to objects in common object-oriented languages is statically verified but cannot be changed at run-time. However, dynamic authorization is required by most applications and it would be desirable to check more flexible access control policies also statically, at least partially. In this work, we introduce a model where “views” to object references represent the current access control...

chapter

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

Luís Caires

Lecture Notes in Computer Science > Foundations of Software Science and Computation Structures > Contributed Papers > 72-89

In addition to behavioral properties, spatial logics can talk about other key properties of concurrent systems such as secrecy, freshness, usage of resources, and distribution. We study an expressive spatial logic for systems specified in the synchronous π-calculus with recursion, based on a small set of behavioral and spatial observations. We give coinductive and equational characterizations of the...

chapter

Types for Dynamic Reconfiguration

João Costa Seco, Luís Caires

Lecture Notes in Computer Science > Programming Languages and Systems > 214-229

We define a core language combining computational and architectural primitives, and study how static typing may be used to ensure safety properties of component composition and dynamic reconfiguration in object-based systems. We show how our language can model typed entities analogous of configuration scripts, makefiles, components, and component instances, where static typing combined with a dynamic...

chapter

Elimination of Quantifiers and Undecidability in Spatial Logics for Concurrency

Luís Caires, Étienne Lozes

Lecture Notes in Computer Science > CONCUR 2004 - Concurrency Theory > Accepted Papers > 240-257

Aiming at a deeper understanding of the essence of spatial logics for concurrency, we study a minimal spatial logic without quantifiers or any operators talking about names. The logic just includes the basic spatial operators void, composition and its adjunct, and the next step modality; for the model we consider a tiny fragment of CCS. We show that this core logic can already encode its own extension...

chapter

Logical Semantics of Types for Concurrency

Luís Caires

Lecture Notes in Computer Science > Algebra and Coalgebra in Computer Science > Invited Talks > 16-35

We motivate and present a logical semantic approach to types for concurrency and to soundness of related systems. The approach is illustrated by the development of a generic type system for the π-calculus, which may be instantiated for specific notions of typing by extension with adequate subtyping principles. Soundness of our type system is established using a logical predicate technique, based on...

INFONA - science communication portal

Search results for: Luís Caires

A Spatial Logic for Concurrency (Part I)

A Basic Model of Typed Components

CONCUR 2007 – Concurrency Theory

Tools and Verification

Conversation Types

The Conversation Calculus: A Model of Service-Oriented Computation

Proof net semantics of proof search computation

Type-Based Access Control in Data-Centric Systems

Verifiable and executable logic specifications of concurrent objects in $$\mathcal{L}_\pi$$

A language for the logical specification of processes and relations

SLWV — A theorem prover for logic programming

Proof-Carrying Code in a Session-Typed Process Calculus

Spatial-Behavioral Types, Distributed Services, and Resources

Subtyping First-Class Polymorphic Components

Session Types as Intuitionistic Linear Propositions

A Type System for Access Control Views in Object-Oriented Languages

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

Types for Dynamic Reconfiguration

Elimination of Quantifiers and Undecidability in Spatial Logics for Concurrency

Logical Semantics of Types for Concurrency

Filter options

Publication date

Content availability

Publication type

Keywords

Data set

Journal

INFONA - science communication portal

Search results for: Luís Caires

Add recipient

Sending message cancelled

Are you sure you want to cancel sending this message?

Send message

Filter options

Publication date

Date range setting

Set the date range to filter the displayed results. You can set a starting date, ending date or both. You can enter the dates manually or choose them from the calendar.

Content availability

Publication type

Keywords

Data set

Journal

Reporting an error / abuse

Sending the report failed

Accessibility options