98 citations · 385 across the 33 of their papers we have counts for
37 papers
FÆRDXEL: An Expert System for Danish Traffic Law
Luís Cruz-Filipe, Jonas Vistrup
We present FÆRDXEL, a tool for symbolic reasoning in the domain of Danish traffic law. FÆRDXEL combines techniques from logic programming with a novel interface that allows users t…
Reasoning about Choreographic Programs
Luís Cruz-Filipe, Eva Graversen, Fabrizio Montesi +1
Choreographic programming is a paradigm where a concurrent or distributed system is developed in a top-down fashion. Programs, called choreographies, detail the desired interaction…
Certified Compilation of Choreographies with hacc
Luís Cruz-Filipe, Lovro Lugović, Fabrizio Montesi
Programming communicating processes is challenging, because it requires writing separate programs that perform compatible send and receive actions at the right time during executio…
Now It Compiles! Certified Automatic Repair of Uncompilable Protocols
Luís Cruz-Filipe, Fabrizio Montesi
Choreographic programming is a paradigm where developers write the global specification (called choreography) of a communicating system, and then a correct-by-construction distribu…
A Formal Theory of Choreographic Programming
Luís Cruz-Filipe, Fabrizio Montesi, Marco Peressotti
Choreographic programming is a paradigm for writing coordination plans for distributed systems from a global point of view, from which correct-by-construction decentralised impleme…
From Infinity to Choreographies: Extraction for Unbounded Systems
Bjørn Angel Kjær, Luís Cruz-Filipe, Fabrizio Montesi
Choreographies are formal descriptions of distributed systems, which focus on the way in which participants communicate. While they are useful for analysing protocols, in practice…
Implementing Choreography Extraction
Luis Cruz-Filipe, Kim S. Larsen, Fabrizio Montesi +1
Choreographies are global descriptions of interactions among concurrent components, most notably used in the settings of verification and synthesis of correct-by-construction softw…
Functional Choreographic Programming
Luís Cruz-Filipe, Eva Graversen, Lovro Lugović +2
Choreographic programming is an emerging programming paradigm for concurrent and distributed systems, whereby developers write the communications that should be enacted and then a…
Formalising a Turing-Complete Choreographic Language in Coq
Luís Cruz-Filipe, Fabrizio Montesi, Marco Peressotti
Theory of choreographic languages typically includes a number of complex results that are proved by structural induction. The high number of cases and the subtle details in some of…
Certifying Choreography Compilation
Luís Cruz-Filipe, Fabrizio Montesi, Marco Peressotti
Choreographic programming is a paradigm for developing concurrent and distributed systems, where programs are choreographies that define, from a global viewpoint, the computations…
Implementing choreography extraction
Luís Cruz-Filipe, Fabrizio Montesi, Larisa Safina
Choreography extraction deals with the generation of a choreography (a global description of communication behaviour) from a set of local process behaviours. In this work, we imple…
Hypothetical answers to continuous queries over data streams
Luís Cruz-Filipe, Graça Gaspar, Isabel Nunes
Continuous queries over data streams may suffer from blocking operations and/or unbound wait, which may delay answers until some relevant input arrives through the data stream. The…
Machine-Assisted Proofs (ICM 2018 Panel)
James Davenport, Bjorn Poonen, James Maynard +3
This submission to arXiv is the report of a panel session at the 2018 International Congress of Mathematicians (Rio de Janeiro, August). It is intended that, while v1 is that repor…
Multiparty Classical Choreographies
Marco Carbone, Luis Cruz-Filipe, Fabrizio Montesi +1
We present Multiparty Classical Choreographies (MCC), a language model where global descriptions of communicating systems (choreographies) implement typed multiparty sessions. Typi…
Connectors meet Choreographies
Farhad Arbab, Luís Cruz-Filipe, Sung-Shik Jongmans +1
We present Cho-Reo-graphies (CR), a new language model that unites two powerful programming paradigms for concurrent software based on communicating processes: Choreographic Progra…
On Asynchrony and Choreographies
Luís Cruz-Filipe, Fabrizio Montesi
Choreographic Programming is a paradigm for the development of concurrent software, where deadlocks are prevented syntactically. However, choreography languages are typically synch…
Communications in Choreographies, Revisited
Luís Cruz-Filipe, Fabrizio Montesi, Marco Peressotti
Choreographic Programming is a paradigm for developing correct-by-construction concurrent programs, by writing high-level descriptions of the desired communications and then synthe…
That's Enough: Asynchrony with Standard Choreography Primitives
Luís Cruz-Filipe, Fabrizio Montesi
Choreographies are widely used for the specification of concurrent and distributed software architectures. Since asynchronous communications are ubiquitous in real-world systems, p…
Efficient Certified RAT Verification
Luís Cruz-Filipe, Marijn Heule, Warren Hunt +2
Clausal proofs have become a popular approach to validate the results of SAT solvers. However, validating clausal proofs in the most widely supported format (DRAT) is expensive eve…
Efficient Certified Resolution Proof Checking
Luís Cruz-Filipe, Joao Marques-Silva, Peter Schneider-Kamp
We present a novel propositional proof tracing format that eliminates complex processing, thus enabling efficient (formal) proof checking. The benefits of this format are demonstra…
The Paths to Choreography Extraction
Luís Cruz-Filipe, Kim S. Larsen, Fabrizio Montesi
Choreographies are global descriptions of interactions among concurrent components, most notably used in the settings of verification (e.g., Multiparty Session Types) and synthesis…
Active Integrity Constraints for Multi-Context Systems
Luís Cruz-Filipe, Graça Gaspar, Isabel Nunes +1
We introduce a formalism to couple integrity constraints over general-purpose knowledge bases with actions that can be executed to restore consistency. This formalism generalizes a…
Grounded Fixpoints and Active Integrity Constraints
Luís Cruz-Filipe
The formalism of active integrity constraints was introduced as a way to specify particular classes of integrity constraints over relational databases together with preferences on…
Choreographies in Practice
Luís Cruz-Filipe, Fabrizio Montesi
Choreographic Programming is a development methodology for concurrent software that guarantees correctness by construction. The key to this paradigm is to disallow mismatched I/O o…