Luís Cruz-Filipe: Publications

Below is a list of my publications, separated by type and within each type in inverse chronological order. Most of them can be downloaded in PDF format; you can also download the BiBTeX reference in case you want to cite it. I also include a selection of submitted publications.
Use the drop-down menu below to view only publications pertaining to a particular topic, or of a particular type.

Topic:

International Publications with Refereeing

[58]Certifying Choreography Compilation (with F. Montesi and M. Peressotti)
in A. Cerone and P. Ölveczky (eds.), Theoreical Aspects of Computing - ICTAC 2021., LNCS 12819:115-133. Springer, September 2021.
DOI 10.1007/978-3-030-85315-0_8

Abstract. Choreographic programming is a paradigm for developing concurrent and distributed systems, where programs are choreographies that define, from a global viewpoint, the computations and interactions that communicating processes should enact. Choreography compilation translates choreographies into the local definitions of process behaviours, given as terms in a process calculus.
Proving choreography compilation correct is challenging and error-prone, because it requires relating languages in different paradigms (global interactions vs local actions) and dealing with a combinatorial explosion of proof cases. We present the first certified program for choreography compilation for a nontrivial choreographic language supporting recursion.

[57]Formalising a Turing-Complete Choreography Language in Coq (with F. Montesi and M. Peressotti)
in L. Cohen and C. Kaliszyk (eds.), Interactive Theorem Proving, ITP 2021., LIPIcs 193:15:1-15:18. Schloss Dagstuhl, June 2021.
DOI 10.4230/LIPIcs.ITP.2021.15

Abstract. The 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 them lead to long reviewing processes, and occasionally to errors being found in published proofs. In this work, we take a published proof of Turing completeness of a choreographic language and formalise it in Coq. Our development includes formalising the choreographic language, its basic properties, Kleene's theory of partial recursive functions, the encoding of these functions as choreographies, and a proof that this encoding is correct.
With this effort, we show that theorem proving can be a very useful tool in the field of choreographic languages: besides the added degree of confidence that we get from a mechanised proof, the formalisation process led us to a significant simplification of the underlying theory. Our results offer a foundation for the future formal development of choreographic languages.

[56]Stratification Approximation Fixpoint Theory and Its Application to Active Integrity Constraints (with B. Bogaerts)
in ACM Transactions on Computational Logic, 22(1):6:1-6:19. ACM, January 2021.
DOI 10.1145/3430750

Abstract. Approximation fixpoint theory (AFT) is an algebraic study of fixpoints of lattice operators that unifies various knowledge representation formalisms. In AFT, stratification of operators has been studied, essentially resulting in a theory that specifies when certain types of fixpoints can be computed stratum per stratum. Recently, novel types of fixpoints related to groundedness have been introduced in AFT. In this paper, we study how those fixpoints behave under stratified operators.
One recent application domain of AFT is the field of active integrity constraints (AICs). We apply our extended stratification theory to AICs and find that existing notions of stratification in AICs are covered by this general algebraic definition of stratification. As a result, we obtain stratification results for a large variety of semantics for AICs.

[55]Hypothetical Answers to Continuous Queries over Data Streams (with G. Gaspar and I. Nunes)
in The 34th AAAI Conference on Artificial Intelligence, AAAI 2020., pages 2798-2805. AAAI Press, February 2020.
DOI 10.1609/aaai.v34i03.5668

Abstract. Continuous queries over data streams often delay answers until some relevant input arrives through the data stream. These delays may turn answers, when they arrive, obsolete to users who sometimes have to make decisions with no help whatsoever. Therefore, it can be useful to provide hypothetical answers - “given the current information, it is possible that X will become true at time t” - instead of no information at all.
In this paper we present a semantics for queries and corresponding answers that covers such hypothetical answers, together with an online algorithm for updating the set of facts that are consistent with the currently available information.

[54]A Core Model for Choreographic Programming (with F. Montesi),
in Theoretical Computer Science, 802:38-66. Elsevier, January 2020.
DOI 10.1016/j.tcs.2019.07.005

Abstract. Choreographic Programming is a paradigm for developing concurrent programs that are deadlock-free by construction, by programming communications declaratively and then synthesising process implementations automatically. Despite strong interest on choreographies, a foundational model that explains which computations can be performed with the hallmark constructs of choreographies is still missing.
In this work, we introduce Core Choreographies (CC), a model that includes only the core primitives of choreographic programming. Every computable function can be implemented as a choreography in CC, from which we can synthesise a process implementation where independent computations run in parallel. We discuss the design of CC and argue that it constitutes a canonical model for choreographic programming.

[53]Formally Verifying the Solution to the Pythagorean Triples Problem (with J. Marques-Silva and P. Schneider-Kamp), © Springer
in Journal of Automated Reasoning, 63(3):695-722. Springer, October 2019.
DOI 10.1007/s10817-018-9490-4

Abstract. The Boolean Pythagorean Triples problem asks: does there exist a binary coloring of the natural numbers such that every Pythagorean triple contains an element of each color? This problem was first solved in 2016, when Heule, Kullmann and Marek encoded a finite restriction of this problem as a propositional formula and showed its unsatisfiability. In this work we formalize their development in the theorem prover Coq. We state the Boolean Pythagorean Triples problem in Coq, define its encoding as a propositional formula and establish the relation between solutions to the problem and satisfying assignments to the formula. We verify Heule et al.'s proof by showing that the symmetry breaks they introduced to simplify the propositional formula are sound, and by implementing a correct-by-construction checker for proofs of unsatisfiability based on reverse unit propagation.

[52]Sorting Networks: to the End and Back Again (with M. Codish, T. Ehlers, M. Müller and P. Schneider-Kamp)
in Journal of Computer and System Sciences, 104:184-201. Elsevier, September 2019.
DOI 10.1016/j.jcss.2016.04.004

Abstract. New properties of the front and back ends of sorting networks are studied, illustrating their utility when searching for bounds on optimal networks. Search focuses first on the “out-sides” of the network and then on the inner part. Previous works focused on properties of the front end to break symmetries in the search. The new, out-side-in, properties shed understanding on how sorting networks sort, and facilitate the computation of new bounds on optimality. We present new, faster, parallel sorting networks for 17–20 inputs. For 17 inputs, we show that no sorting network using less layers exists.

[51]Multiparty Classical Choreographies (with M. Carbone, F. Montesi and A. Murawska) © Springer
in F. Mesnard and P.J. Stuckey (eds.), Logic-Based Program Synthesis and Transformation (LOPSTR 2018)., LNCS 11408:59-76. Springer, May 2019.
DOI 10.1007/978-3-030-13838-7_4

Abstract. We present Multiparty Classical Choreographies (MCC), a language model where global descriptions of communicating systems (choreographies) and processes can be modularly composed to implement typed multiparty sessions. Typing is achieved by generalising classical linear logic to judgements that explicitly record parallelism by means of hypersequents. Our approach unifies different lines of work on choreographies and processes with multiparty sessions, as well as their connection to linear logic. Thus, results developed in one context are carried over to the others. Key novelties of MCC include support for behavioural polymorphism in choreographies, as well as a translation from processes with replication to choreographies.

[50] Machine-Assisted Proofs (with J. Davenport, B. Poonen, J. Maynard, H. Helfgott and P.H. Tiep),
in B. Sirakov, P. Ney de Souza and M. Viana (eds.), Proceedings of the International Congress of Mathematicians (ICM 2018), volume 1, pages 1085-1110. World Scientific, May 2019.
DOI 10.1142/11060

Abstract. This panel took place on Tuesday 7th August 2018. After the moderator had introduced the topic, the panelists presented their experiences and points of view, and then took questions from the floor.

[49]Complete and Efficient DRAT Proof Checking (with A. Rebola-Pardo)
in N. Björner and A. Gurfinkel (eds.), Formal Methods for Computer-Aided Design (FMCAD 2018), pages 1-9. IEEE, October 2018.
DOI 10.23919/FMCAD.2018.8602993

Abstract. DRAT proofs have become the standard for verifying unsatisfiability proofs emitted by modern SAT solvers. However, recent work showed that the specification of the format differs from its implementation in existing tools due to optimizations necessary for efficiency. Although such differences do not compromise soundness of DRAT checkers, the sets of correct proofs according to the specification and to the implementation are incomparable. We discuss how it is possible to design DRAT checkers faithful to the specification by carefully modifying the standard optimization techniques. We implemented such modifications in a configurable DRAT checker. Our experimental results show negligible overhead due to these modifications, suggesting that efficient verification of the DRAT specification is possible. Furthermore, we show that the differences between specification and implementation of DRAT often arise in practice.

[48]Active Integrity Constraints for General-Purpose Knowledge Bases (with G. Gaspar, I. Nunes and P. Schneider-Kamp) © Springer
in Annals of Mathematics and Artificial Intelligence, 83(3-4):213-246. Springer, August 2018.
DOI 10.1007/s10472-018-9577-y

Abstract. In the database world, integrity constraints are essential to guarantee database integrity. The related problem of database repair deals with finding the best way to change a database so that it satisfies its integrity constraints. These two topics have been studied intensively since the 1980s. The formalism of active integrity constraints, proposed in 2004, aims at addressing them jointly, by providing a syntax whereby a particular subclass of integrity constraints can be specified together with preferred ways to repair inconsistency.
In the last decade, several authors have proposed adaptations of the notion of integrity constraints to other reasoning frameworks than relational databases. In this article, we extend this line of work in two ways. First, we target multi-context systems, a general-purpose framework for combining heterogeneous reasoning systems, able to model most other reasoning frameworks, as we demonstrate. Second, we extend the notions of active integrity constraints and grounded repairs to this generalized setting. This way of including repair suggestions inside integrity constraints, subject to a validity check, enables us to define simple iterative algorithms to find all possible grounded repairs for an inconsistent multi-context system, avoiding the need to solve complex or undecidable problems.

[47]Communications in Choreographies, Revisited (with F. Montesi and M. Peressotti)
in H.M. Haddad, R.L. Wainright and R. Chbeir (eds.), Proceedings of the Symposium on Applied Computing, SAC 2018, Pau, France, April 9-13, 2018, pages 1248-1255. ACM, 2018.
DOI 10.1145/3167132.3167267

Abstract. Choreographic Programming is a paradigm for developing correct-by-construction concurrent programs, by writing high-level descriptions of the desired communications and then synthesising process implementations automatically. So far, choreographic programming has been explored in the monadic setting: interaction terms express point-to-point communications of a single value. However, real-world systems often rely on interactions of polyadic nature, where multiple values are communicated among two or more parties, like multicast, scatter-gather, and atomic exchanges.
We introduce a new model for choreographic programming equipped with a primitive for grouped interactions that subsumes all the above scenarios. Intuitively, grouped interactions can be thought of as being carried out as one single interaction. In practice, they are implemented by processes that carry them out in a concurrent fashion. After formalising the intuitive semantics of grouped interactions, we prove that choreographic programs and their implementations are correct and deadlock-free by construction.

[46]Fixpoint Semantics for Active Integrity Constraints (with B. Bogaerts)
in Artificial Intelligence, 255:43-70. Elsevier, February 2018.
DOI 10.1016/j.artint.2017.11.003

Abstract. Active integrity constraints (AICs) constitute a formalism to associate with a database not just the constraints it should adhere to, but also how to fix the database in case one or more of these constraints are violated. The intuitions regarding which repairs are “good” given such a description are closely related to intuitions that live in various areas of non-monotonic reasoning, such as logic programming and autoepistemic logic.
In this paper, we apply approximation fixpoint theory, an abstract, algebraic framework designed to unify semantics of non-monotonic logics, to the field of AICs. This results in a new family of semantics for AICs. We study properties of our new semantics and relationships to existing semantics. In particular, we argue that two of the newly defined semantics stand out. Grounded repairs have a simple definition that is purely based on semantic principles that semantics for AICs should adhere to. And, as we show, they coincide with the intended interpretation of AICs on many examples. The second semantics of interest is the AFT-well-founded semantics: it is a computationally cheap semantics that provides upper- and lower bounds for many other classes of repairs.

[45]On Asynchrony and Choreographies (with F. Montesi)
in M. Bartoletti, L. Bocchi, L. Henrio and S. Knight (eds.), Proceedings 10th Interaction and Concurrency Experience. EPTCS 261:76-90. Open Publishing Association, 2017.
DOI 10.4204/EPTCS.261.8

Abstract. Choreographic Programming is a paradigm for the development of concurrent software, where deadlocks are prevented syntactically. However, choreography languages are typically synchronous, whereas many real-world systems have asynchronous communications. Previous attempts at enriching choreographies with asynchrony rely on ad-hoc constructions, whose adequacy is only argued informally. In this work, we formalise the properties that an asynchronous semantics for choreographies should have: messages can be sent without the intended receiver being ready, and all sent messages are eventually received. We explore how out-of-order execution, used in choreographies for modelling concurrency, can be exploited to endow choreographies with an asynchronous semantics. Our approach satisfies the properties we identified. We show how our development yields a pleasant correspondence with FIFO-based asynchronous messaging, modelled in a process calculus, and discuss how it can be adopted in more complex choreography models.

[44]Formally Proving Size Optimality of Sorting Networks (with K.S. Larsen and P. Schneider-Kamp), © Springer
in Journal of Automated Reasoning, 59(4):425-454. Springer, December 2017.
DOI 10.1007/s10817-017-9405-9

Abstract. Recent successes in formally verifying increasingly larger computer-generated proofs have relied extensively on (a) using oracles, to find answers for recurring subproblems efficiently, and (b) extracting formally verified checkers, to perform exhaustive case analysis in feasible time.
In this work we present a formal verification of optimality of sorting networks on up to 9 inputs, making it one of the largest computer-generated proofs that has been formally verified. We show that an adequate pre-processing of the information provided by the oracle is essential for feasibility, as it improves the time required by our extracted checker by several orders of magnitude.

[43]How to Get More Out of Your Oracles (with K.S. Larsen and P. Schneider-Kamp), © Springer
in M. Ayala-Rincon and C. Muñoz (eds.), Interactive Theorem Proving, ITP 2017, LNCS 10499:164-170. Springer, September 2017.
DOI 10.1007/978-3-319-66107-0_11

Abstract. Formal verification of large computer-generated proofs often relies on certified checkers based on oracles. We propose a methodology for such proofs, advocating a separation of concerns between formalizing the underlying theory and optimizing the algorithm implemented in the checker, based on the observation that such optimizations can benefit significantly from adequately adapting the oracle.

[42]Semantics for Active Integrity Constraints Using Approximation Fixpoint Theory (with B. Bogaerts)
in C. Sierra (ed.), 26th International Joint Conference on Artificial Intelligence, IJCAI 2017, pages 866-872. IJCAI, 2017.
DOI 10.24963/ijcai.2017/120

[41]Efficient Certified RAT Verification (with M.J.H. Heule, W.A. Hunt Jr., M. Kaufmann and P. Schneider-Kamp) © Springer
in L. de Moura (ed.), Automated Deduction - CADE 26, LNAI 10395:220-236. Springer, August 2017.
DOI 10.1007/978-3-319-63046-5_14

Abstract. 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 even in highly optimized implementations. We present a new format, called LRAT, which extends the DRAT format with hints that facilitate a simple and fast validation algorithm. Checking validity of LRAT proofs can be implemented using trusted systems such as the languages supported by theorem provers. We demonstrate this by implementing two certified LRAT checkers, one in Coq and one in ACL2.

[40]That's Enough: Asynchrony with Standard Choreography Primitives (with F. Montesi)
in C. Caleiro, F. Dionísio, P. Gouveia, P. Mateus and J. Rasga (eds.), Logic and Computation: Essays in Honour of Amílcar Sernadas, volume 33 of Tributes, pages 125-142, College Publications, 2017.

Abstract. Choreographies are widely used for the specification of concurrent and distributed software architectures. Since asynchronous communications are ubiquitous in real-world systems, previous works have proposed different approaches for the formal modelling of asynchrony in choreographies. Such approaches typically rely on ad-hoc syntactic terms or semantics for capturing the concept of messages in transit, yielding different formalisms that have to be studied separately.
In this work, we take a different approach, and show that such extensions are not needed to reason about asynchronous communications in choreographies. Rather, we demonstrate how a standard choreography calculus already has all the needed expressive power to encode messages in transit (and thus asynchronous communications) through the primitives of process spawning and name mobility. The practical consequence of our results is that we can reason about real-world systems within a choreography formalism that is simpler than those hitherto proposed.

[39]Procedural Choreographic Programming (with F. Montesi) © Springer
in A. Bouajjani and A. Silva (eds.), Formal Techniques for Distributed Objects, Components, and Systems – 37th IFIP WG 6.1 International Conference, FORTE 2017, LNCS 10321:92-107. Springer, June 2017.
DOI 10.1007/978-3-319-60225-7_7

Abstract. Choreographic Programming is an emerging paradigm for correct-by-construction concurrent programming. However, its applicability is limited by the current lack of support for reusable procedures.
We propose Procedural Choreographies (PC), a choreographic language model with full procedural abstraction. PC includes unbounded process creation and name mobility, yielding a powerful framework for writing correct concurrent algorithms that can be compiled into a process calculus. This increased expressivity requires a typing discipline to ensure that processes are properly connected when enacting procedures.

[38]Encoding Asynchrony in Choreographies (with F. Montesi) (poster )
in D. Shin and M. Lencastre (eds.), Proceedings of the Symposium on Applied Computing, SAC 2017, Marrakech, Morocco, April 3-7, 2017, pages 1175-1177. ACM, 2017.
DOI 10.1145/3019612.3019901

[37]Formally Proving the Boolean Pythagorean Triples Conjecture (with P. Schneider-Kamp)
in T. Eiter and D Sands (eds.), Proceedings of LPAR-21, EPiC Series in Computing 46:509-522. EasyChair Publications, May 2017.

Abstract. In 2016, Heule, Kullmann and Marek solved the Boolean Pythagorean Triples problem: is there a binary coloring of the natural numbers such that every Pythagorean triple contains an element of each color? By encoding a finite portion of this problem as a propositional formula and showing its unsatisfiability, they established that such a coloring does not exist. Subsequently, this answer was verified by a correct-by-construction checker extracted from a Coq formalization, which was able to reproduce the original proof. However, none of these works address the question of formally addressing the relationship between the propositional formula that was constructed and the mathematical problem being considered. In this work, we formalize the Boolean Pythagorean Triples problem in Coq. We recursively define a family of propositional formulas, parameterized on a natural number n, and show that unsatisfiability of this formula for any particular n implies that there does not exist a solution to the problem. We then formalize the mathematical argument behind the simplification step in the original proof of unsatisfiability and the logical argument underlying cube-and-conquer, obtaining a verified proof of Heule et al.'s solution.

[36]Optimizing Sorting Algorithms by Using Sorting Networks (with M. Codish, M. Nebel and P. Schneider-Kamp), © Springer
in Formal Aspects of Computing, 29(3):559-579. Springer, May 2017.
DOI 10.1007/s00165-016-0401-3

Abstract. In this paper, we show how the theory of sorting networks can be applied to synthesize optimized general-purpose sorting libraries. Standard sorting libraries are often based on combinations of the classic Quicksort algorithm, with insertion sort applied as base case for small, fixed, numbers of inputs. Unrolling the code for the base case by ignoring loop conditions eliminates branching, resulting in code equivalent to a sorting network. By replacing it with faster sorting networks, we can improve the performance of these algorithms. We show that by considering the number of comparisons and swaps alone we are not able to predict any real advantage of this approach. However, significant speed-ups are obtained when taking advantage of instruction level parallelism and non-branching conditional assignment instructions, both of which are common in modern CPU architectures. Furthermore, a close control of how often registers have to be spilled to memory gives us a complete explanation of the performance of different sorting networks, allowing us to choose an optimal one for each particular architecture. Our experimental results show that using code synthesized from these efficient sorting networks as the base case for Quicksort libraries results in significant real-world speed-ups.

[35]A Core Model for Choreographic Programming (with F. Montesi), © Springer
in O. Kouchnarenko and R. Khosravi (eds.), Formal Aspects of Component Software – 13th International Conference, FACS 2016, LNCS 10231:17-35. Springer, April 2017.
DOI 10.1007/978-3-319-57666-4_3

[34]Efficient Certified Resolution Proof Checking (with J. Marques-Silva and P. Schneider-Kamp), © Springer
in A. Legay and T. Margaria (eds.), Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2017, LNCS 10205:118-135. Springer, April 2017.
DOI 10.1007/978-3-662-54577-5_7

Abstract. We present a novel propositional proof tracing format that eliminates complex processing, thus enabling efficient (formal) proof checking. The benefits of this format are demonstrated by implementing a proof checker in C, which outperforms a state-of-the-art checker by two orders of magnitude. We then formalize the theory underlying propositional proof checking in Coq, and extract a correct-by-construction proof checker for our format from the formalization. An empirical evaluation using 280 unsatisfiable instances from the 2015 and 2016 SAT competitions shows that this certified checker usually performs comparably to a state-of-the-art non-certified proof checker. Using this format, we formally verify the recent 200 TB proof of the Boolean Pythagorean Triples conjecture.

[33]The Paths to Choreography Extraction (with K.S. Larsen and F. Montesi), © Springer
in J. Esparza and A.S. Murawski (eds.), Foundations of Software Science and Computation Structures, FoSSaCS 2017, LNCS 10203:424-440. Springer, April 2017.
DOI 10.1007/978-3-662-54458-7_25

Abstract. Choreographies are global descriptions of interactions among concurrent components, most notably used in the settings of verification (e.g., Multiparty Session Types) and synthesis of correct-by-construction software (Choreographic Programming). They require a top-down approach: programmers first write choreographies, and then use them to verify or synthesize their programs. However, most existing software does not come with choreographies yet, which prevents their application.
To attack this problem, we propose a novel methodology (called choreography extraction) that, given a set of programs or protocol specifications, automatically constructs a choreography that describes their behavior. The key to our extraction is identifying a set of paths in a graph that represents the symbolic execution of the programs of interest. Our method improves on previous work in several directions: we can now deal with programs that are equipped with a state and internal computation capabilities; time complexity is dramatically better; we capture programs that are correct but not necessarily synchronizable, i.e., they work because they exploit asynchronous communication.

[32]From Description-Logic Programs to Multi-Context Systems (with G. Gaspar and I. Nunes).
Journal of Logical and Algebraic Methods in Programming, 88:26-44. Elsevier, April 2017.
DOI 10.1016/j.jlamp.2017.01.005

Abstract. The combination of logic program-style rules with other reasoning systems has been a fertile topic of research in the last years, with the proposal of several different systems that achieve this goal. In this work, we look at two of these systems, dl-programs and multi-context systems, which address different aspects of this combination, and include different, incomparable programming constructs. We prove that every dl-program can be transformed into a multi-context system in such a way that the different semantics for each paradigm are naturally related. As a consequence, constructions developed for dl-programs can be automatically ported to multi-context systems. In particular, we show how to model default rules over ontologies with the usual semantics.

[31]Optimal-Depth Sorting Networks (with D. Bundala, M. Codish, P. Schneider-Kamp and J. Závodný)
Journal of Computer and System Sciences, 84:185-204. Elsevier, March 2017.
DOI 10.1016/j.jcss.2016.09.004

Abstract. We solve a 40-year-old open problem on the depth optimality of sorting networks. In 1973, Donald E. Knuth detailed, in Volume 3 of The Art of Computer Programming, sorting networks of the smallest depth known at the time for n≤16 inputs, quoting optimality for n≤8. In 1989, Parberry proved the optimality of the networks with 9≤n≤10 inputs. In this article, we present a general technique for obtaining such optimality results, and use it to prove the optimality of the remaining open cases of 11≤n≤16 inputs. We show how to exploit symmetry to construct a small set of two-layer networks on n inputs such that if there is a sorting network on n inputs of a given depth, then there is one whose first layers are in this set. For each network in the resulting set, we construct a propositional formula whose satisfiability is necessary for the existence of a sorting network of a given depth. Using an off-the-shelf SAT solver we show that the sorting networks listed by Knuth are optimal. For n≤10 inputs, our algorithm is orders of magnitude faster than the prior ones.

[30]Active Integrity Constraints: from Theory to Implementation (with M. Franz, A. Hakhverdyan, M. Ludovico, I. Nunes and P. Schneider-Kamp), © Springer
in A. Fred, J. Dietz, D. Aveiro, K. Liu and J. Filipe (eds.), Knowledge Discovery, Knowledge Engineering and Knowledge Management (IC3K2015), CCIS 631:399-420. Springer, December 2016.
DOI 10.1007/978-3-319-52758-1_22

Abstract. The problem of database consistency relative to a set of integrity constraints has been extensively studied since the 1980s, and is still recognized as one of the most important and complex in the field. In recent years, with the proliferation of knowledge repositories (not only databases) in practical applications, there has also been an effort to develop implementations of consistency maintenance algorithms that have a solid theoretical basis.
The framework of active integrity constraints (AICs) is one example of such an effort, providing theoretical grounds for rule-based algorithms for ensuring database consistency. An AIC consists of an integrity constraint together with a specification of actions that may be taken to repair a database that does not satisfy it. Both denotational and operational semantics have been proposed for AICs.
In this paper, we describe repAIrC, a prototype implementation of the algorithms previously proposed targetting SQL databases, i.e., the most prolific type of databases. Using repAIrC, we can both validate an SQL database with respect to a given set of AICs and compute possible repairs in case the database is inconsistent; the tool is able to work with the different kinds of repairs that have been considered, and achieves optimal asymptotic complexity in their computation. It also implements strategies for parallelizing the search for repairs, which in many cases can make untractable problems become easily solvable.

[29]Active Integrity Constraints for Multi-context Systems (with G. Gaspar, I. Nunes and P. Schneider-Kamp), © Springer
in E. Blomqvist, F. Vitali, P. Ciancatini and F. Poggi (eds.), Knowledge Engineering and Knowledge Management – 20th International Conference, EKAW 2016, LNAI 10024:98-112, Springer, November 2016.
DOI: 10.1007/978-3-319-49004-5_7

Abstract. 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 active integrity constraints over databases. In the more general setting of multi-context systems, adding repair suggestions to integrity constraints allows defining simple iterative algorithms to find all possible grounded repairs – repairs for the global system that follow the suggestions given by the actions in the individual rules. We apply our methodology to ontologies, and show that it can express most relevant types of integrity constraints in this domain.

[28]Grounded Fixpoints and Active Integrity Constraints
in M. Carro, A. King, M. De Vos and N. Saeedloei (eds.), Technical Communications of the 32nd International Conference on Logic Programming (ICLP'16), OASIcs 52:11.1-11.14, Schloss Dagstuhl, November 2016.
DOI 10.4230/OASIcs.ICLP.2016.11

Abstract. 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 how to repair existing inconsistencies. The rule-based syntax of such integrity constraints also provides algorithms for finding such repairs that achieve the best asymptotic complexity.
However, the different semantics that have been proposed for these integrity constraints all exhibit some counter-intuitive examples. In this work, we look at active integrity constraints using ideas from algebraic fixpoint theory. We show how database repairs can be modeled as fixpoints of particular operators on databases, and study how the notion of grounded fixpoint induces a corresponding notion of grounded database repair that captures several natural intuitions, and in particular avoids the problems of previous alternative semantics.
In order to study grounded repairs in their full generality, we need to generalize the notion of grounded fixpoint to non-deterministic operators. We propose such a definition and illustrate its plausibility in the database context.

[27]Choreographies in Practice (with F. Montesi), © Springer
in E. Albert and I. Lanesi (eds.), Formal Techniques for Distributed Objects, Components, and Systems – 36th IFIP WG 6.1 International Conference, FORTE 2016, LNCS 9688:114-123. Springer, June 2016.
DOI 10.1007/978-3-319-39570-8_8

Abstract. 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 operations in programs, and mechanically synthesise process implementations.
There is still a lack of practical illustrations of the applicability of choreographies to computational problems with standard concurrent solutions. In this work, we explore the potential of choreographic programming by writing concurrent algorithms for sorting, solving linear equations, and computing Fast Fourier Transforms. The lessons learned from this experiment give directions for future improvements of the paradigm.

[26]Sorting Nine Inputs Requires Twenty-Five Comparisons (with M. Codish, M. Frank and P. Schneider-Kamp)
Journal of Computer and System Sciences, 82(3):551-563. Elsevier, May 2016.
DOI 10.1016/j.jcss.2015.11.014

Abstract. This paper describes a computer-assisted non-existence proof of 9-input sorting networks consisting of 24 comparators, hence showing that the 25-comparator sorting network found by Floyd in 1964 is optimal. As a corollary, the 29-comparator network found by Waksman in 1969 is optimal when sorting 10 inputs.
This closes the two smallest open instances of the optimal-size sorting network problem, which have been open since the results of Floyd and Knuth from 1966 proving optimality for sorting networks of up to 8 inputs.

[25]Integrity Constraints for General-Purpose Knowledge Bases (with I. Nunes and P. Schneider-Kamp), © Springer
in M. Gyssens and G. Simari (eds.), Foundations of Information and Knowledge Systems – 9th International Symposium, FoIKS 2016, LNCS 9616:235-254. Springer, March 2016.
DOI 10.1007/978-3-319-30024-5_13

Abstract. Integrity constraints in databases have been studied extensively since the 1980s, and they are considered essential to guarantee database integrity. In recent years, several authors have studied how the same notion can be adapted to reasoning frameworks, in such a way that they achieve the purpose of guaranteeing a system's consistency, but are kept separate from the reasoning mechanisms.
In this paper we focus on multi-context systems, a general-purpose framework for combining heterogeneous reasoning systems, enhancing them with a notion of integrity constraints that generalizes the corresponding concept in the database world.

[24]Applying Sorting Networks to Synthesize Optimized Sorting Libraries (with M. Codish, M. Nebel and P. Schneider-Kamp), © Springer
in M. Falaschi (ed.), Logic-Based Program Synthesis and Transformation (LOPSTR 2015), LNCS 9527:127-142. Springer, December 2015.
DOI 10.1007/978-3-319-27436-2_8

Abstract. This paper shows an application of the theory of sorting networks to facilitate the synthesis of optimized general purpose sorting libraries. Standard sorting libraries are often based on combinations of the classic Quicksort algorithm with insertion sort applied as the base case for small fixed numbers of inputs. Unrolling the code for the base case by ignoring loop conditions eliminates branching and results in code which is equivalent to a sorting network. This enables the application of further program transformations based on sorting network optimizations, and eventually the synthesis of code from sorting networks. We show that if considering the number of comparisons and swaps then theory predicts no real advantage of this approach. However, significant speed-ups are obtained when taking advantage of instruction level parallelism and non-branching conditional assignment instructions, both of which are common in modern CPU architectures. We provide empirical evidence that using code synthesized from efficient sorting networks as the base case for Quicksort libraries results in significant real-world speed-ups.

[23]repAIrC: A Tool for Ensuring Data Consistency by Means of Active Integrity Constraints (with M. Franz, A. Hakhverdyan, M. Ludovico, I. Nunes and P. Schneider-Kamp)
in A. Fred, J. Dietz, D. Aveiro, K. Liu and J. Filipe (eds.), Proceedings of the 7th International Joint Conference on Knowledge Discovery, Knowledge Engineering and Knowledge Management (IC3K 2015), volume 3, pages 17-26. SCITEPRESS, November 2015.
DOI 10.5220/0005586400170026

Abstract. Consistency of knowledge repositories is of prime importance in organization management. Integrity constraints are a well-known vehicle for specifying data consistency requirements in knowledge bases; in particular, active integrity constraints go one step further, allowing the specification of preferred ways to overcome inconsistent situations in the context of database management.
This paper describes a tool to validate an SQL database with respect to a given set of active integrity constraints, proposing possible repairs in case the database is inconsistent. The tool is able to work with the different kinds of repairs proposed in the literature, namely simple, founded, well-founded and justified repairs. It also implements strategies for parallelizing the search for them, allowing the user both to compute partitions of independent or stratified active integrity constraints, and to apply these partitions to find repairs of inconsistent databases efficiently in parallel.

[22]Formalizing Size-Optimal Sorting Networks: Extracting a Certified Proof Checker (with P. Schneider-Kamp), © Springer
in C. Urban and X. Zhang (eds.), Interactive Theorem Proving, ITP 2015, LNCS 9236:154-169. Springer, August 2015.
DOI 10.1007/978-3-319-22102-1_10

Abstract. Since the proof of the four color theorem in 1976, computer-generated proofs have become a reality in mathematics and computer science. During the last decade, we have seen formal proofs using verified proof assistants being used to verify the validity of such proofs.
In this paper, we describe a formalized theory of size-optimal sorting networks. From this formalization we extract a certified checker that successfully verifies computer-generated proofs of optimality on up to 8 inputs. The checker relies on an untrusted oracle to shortcut the search for witnesses on more than 1.6 million NP-complete subproblems.

[21]Optimizing a Certified Proof Checker for a Large-Scale Computer-Generated Proof (with P. Schneider-Kamp), © Springer
in M. Kerber, J. Carette, C. Kaliszyk, F. Rabe and V. Sorge (eds.), Intelligent Computer Mathematics, CICM 2015, LNAI 9150:55-70. Springer, July 2015.
DOI 10.1007/978-3-319-20615-8_4

Abstract. In recent work, we formalized the theory of optimal-size sorting networks with the goal of extracting a verified checker for the large-scale computer-generated proof that 25 comparisons are optimal when sorting 9 inputs, which required more than a decade of CPU time and produced 27 GB of proof witnesses. The checker uses an untrusted oracle based on these witnesses and is able to verify the smaller case of 8 inputs within a couple of days, but it did not scale to the full proof for 9 inputs.
In this paper, we describe several non-trivial optimizations of the algorithm in the checker, obtained by appropriately changing the formalization and capitalizing on the symbiosis with an adequate implementation of the oracle. We provide experimental evidence of orders of magnitude improvements to both runtime and memory footprint for 8 inputs, and actually manage to check the full proof for 9 inputs.

Awarded best paper in the proceedings of CICM 2015 (CALCULEMUS track)

[20]Design Patterns for Description-logic Programs (with G. Gaspar and I. Nunes), © Springer
in A. Fred, J. Dietz, K. Liu and J. Filipe (eds.), Knowledge Discovery, Knowledge Engineering and Knowledge Management (IC3K2013), CCIS 454:199-214. Springer, April 2015.
DOI 10.1007/978-3-662-46549-3_13

Abstract. Originally proposed in the mid-90s, design patterns for software development played a key role in object-oriented programming not only in increasing software quality, but also by giving a better understanding of the power and limitations of this paradigm. Since then, several authors have endorsed a similar task for other programming paradigms, in the hope of achieving similar benefits.
In this paper we present a set of design patterns for Mdl-programs, a hybrid formalism combining several description logic knowledge bases via a logic program. These patterns are extensively applied in a natural way in a large-scale example that illustrates how their usage greatly simplifies some programming tasks, at the level of both development and extension.
We also discuss some limitations of this formalism, examining some usual patterns in other programming paradigms that have no parallel in Mdl-programs.

[19]The Finitistic Consistency of Heck's Predicative Fregean System (with F. Ferreira)
Notre Dame Journal of Formal Logic, 56(1):61-79, 2015.
DOI 10.1215/00294527-2835110

Abstract. Frege's theory is inconsistent (Russell's paradox). However, the predicative version of Frege's system is consistent. This was proved by Richard Heck in 1996 using a model theoretic argument. In this paper, we give a finitistic proof of this consistency result. As a consequence, Heck's predicative theory is rather weak (as was suspected). We also prove the finitistic consistency of the extension of Heck's theory to Δ¹₁-comprehension and of Heck's ramified predicative second-order system.

[18]Sorting Networks: the End Game (with M. Codish and P. Schneider-Kamp), © Springer
in A.-H. Dediu, E. Formenti, C. Martín-Vide and B. Truthe (eds.), Language and Automata Theory and Applications, 9th International Conference, LATA 2015, LNCS 8977:664-675. Springer, March 2015.
DOI 10.1007/978-3-319-15579-1_52

Abstract. This paper studies properties of the back end of a sorting network and illustrates the utility of these in the search for networks of optimal size or depth. All previous works focus on properties of the front end of networks and on how to apply these to break symmetries in the search. The new properties help shed understanding on how sorting networks sort and speed-up solvers for both optimal size and depth by an order of magnitude.

[17]Twenty-Five Comparators is Optimal when Sorting Nine Inputs (and Twenty-Nine for Ten) (with M. Codish, M. Frank and P. Schneider-Kamp)
26th IEEE International Conference on Tools with Artificial Intelligence, ICTAI 2014, pages 186-193. IEEE, December 2014.
DOI 10.1109/ICTAI.2014.36

Abstract. This paper describes a computer-assisted non-existence proof of nine-input sorting networks consisting of 24 comparators, hence showing that the 25-comparator sorting network found by Floyd in 1964 is optimal. As a corollary, we obtain that the 29-comparator network found by Waksman in 1969 is optimal when sorting ten inputs.
This closes the two smallest open instances of the optimal size sorting network problem, which have been open since the results of Floyd and Knuth from 1966 proving optimality for sorting networks of up to eight inputs.
The proof involves a combination of two methodologies: one based on exploiting the abundance of symmetries in sorting networks, and the other, based on an encoding of the problem to that of satisfiability of propositional logic. We illustrate that, while each of these can single handed solve smaller instances of the problem, it is their combination which leads to an efficient solution for nine inputs.

[16]Information Flow within Relational Multi-context Systems (with G. Gaspar and I. Nunes), © Springer
in K. Janowicz, S. Schlobach, P. Lambrix and E. Hyvönen (eds.), Knowledge Engineering and Knowledge Management – 19th International Conference, EKAW 2014, LNAI 8876:97-108. Springer, November 2014.
DOI 10.1007/978-3-319-13704-9_8

Abstract. Multi-context systems (MCSs) are an important framework for heterogeneous combinations of systems within the Semantic Web. In this paper, we propose generic constructions to achieve specific forms of interaction in a principled way, and sistematize some useful techniques to work with ontologies within an MCS. All these mechanisms are presented in the form of general-purpose design patterns. Their study also suggests new ways in which this framework can be further extended.

[15]The Quest for Optimal Sorting Networks: Efficient Generation of Two-Layer Prefixes (with M. Codish and P. Schneider-Kamp)
in F. Winkler, V. Negru, T. Ida, T. Jebelan, D. Petcu, S.M. Watt and D. Zaharie (eds.), 16th International Symposium on Symbolic and Numerical Algorithms for Scientific Computing, SYNASC 2014, pages 359-366. IEEE, October 2014.
DOI 10.1109/SYNASC.2014.55

Abstract. Previous work identifying depth-optimal n-channel sorting networks for 9≤n≤16 is based on exploiting symmetries of the first two layers. However, the naive generate-and-test approach typically applied does not scale. This paper revisits the problem of generating two-layer prefixes modulo symmetries. An improved notion of symmetry is provided and a novel technique based on regular languages and graph isomorphism is shown to generate the set of non-symmetric representations. An empirical evaluation demonstrates that the new method outperforms the generate-and-test approach by orders of magnitude and easily scales until n=40.

[14]The Stream-based Service-Centered Calculus: a Foundation for Service-Oriented Programming (with I. Lanese, F. Martins, A. Ravara, and V. Vasconcelos), © Springer
in Formal Aspects of Computing, 26:865-918. Springer, September 2014.
DOI 10.1007/s00165-013-0284-5

Abstract. We give a formal account of SSCC, a calculus for modeling service-based systems, suitable to describe both service composition (orchestration) and the protocols that services follow when invoked (conversation). The calculus includes primitives for defining and invoking services, for isolating conversations (called sessions) among clients and servers, and for orchestrating services. The calculus is equipped with a reduction and a labeled transition semantics related by an equivalence result.
SSCC provides a good trade-off between expressive power for modeling and simplicity for analysis. We assess the expressive power by modeling van der Aalst workflow patterns and an automotive case study from the European project Sensoria. For analysis, we present a simple type system ensuring compatibility of client and service protocols. We also study the behavioral theory of the calculus, highlighting some axioms that capture the behavior of the different primitives.
As a final application of the theory, we define and prove correct some program transformations. These allow to start modeling a system from a typical UML Sequence Diagram, and then transform the specification to match the service-oriented programming style, thus simplifying its implementation using web services technology.

Included as a Notable Article in Computing in Computing Reviews' 19th Annual Best of Computing list.

[13]Optimizing Computation of Repairs from Active Integrity Constraints, © Springer
in C. Beierle and C. Meghini (eds.), Foundations of Information and Knowledge Systems – 8th International Symposium, FoIKS 2014, LNCS 8367:361-380. Springer, March 2014.
DOI 10.1007/978-3-319-04939-7_18

Abstract. Active integrity constraints (AICs) are a form of integrity constraints for databases that not only identify inconsistencies, but also suggest how these can be overcome. The semantics for AICs defines different types of repairs, but deciding whether an inconsistent database can be repaired and finding possible repairs is a NP- or Σ^p₂-complete problem, depending on the type of repairs one has in mind. In this paper, we introduce two different relations on AICs: an equivalence relation of independence, allowing the search to be parallelized among the equivalence classes, and a precedence relation, inducing a stratification that allows repairs to be built progressively. Although these relations have no impact on the worst-case scenario, they can make significant difference in the practical computation of repairs for inconsistent databases.

[12]Description logics, Rules and Multi-context Systems (with R. Henriques and I. Nunes), © Springer
in K. McMillan, A. Middeldorp, and A. Voronkov (eds.), Logic for Programming, Artificial Intelligence, and Reasoning, 19th International Conference, LPAR-19, LNCS 8312:243-257. Springer, December 2013.
DOI 10.1007/978-3-642-45221-5_18

Abstract. The combination of rules and ontologies has been a fertile topic of research in the last years, with the proposal of several different systems that achieve this goal. In this paper, we look at two of these mechanisms, Mdl-programs and multi-context systems, which address different aspects of this combination, and include different, incomparable programming constructs. Despite this, we show that every Mdl-program can be transformed in a multi-context system, and this transformation relates the different semantics for each paradigm in a natural way. As an application, we show how a set of design patterns for multi-context systems can be obtained from previous work on Mdl-programs.

[11]Patterns for Interfacing between Logic Programs and Multiple Ontologies (with I. Nunes and G. Gaspar)
in J. Filipe and J. Dietz (eds.), International Conference on Knowledge Engineering and Ontology Development (KEOD2013), pages 58-69. SCITEPRESS, September 2013.
DOI 10.5220/0004544100580069

Abstract. Originally proposed in the mid-90s, design patterns for software development played a key role in object-oriented programming not only in increasing software quality, but also by giving a better understanding of the power and limitations of this paradigm. Since then, several authors have endorsed a similar task for other programming paradigms, in the hope of achieving similar benefits.
In this paper we discuss design patterns for hybrid semantic web systems combining several description logic knowledge bases via a logic program. We introduce eight design patterns, grouped in three categories: three elementary patterns, which are the basic building blocks; four derived patterns, built from these; and a more complex pattern, the study of which can shed some insight in future syntactic developments of the underlying framework. These patterns are extensively applied in a natural way in a large-scale example that illustrates how their usage greatly simplifies some programming tasks, at the level of both development and extension.
We work in a generalization of dl-programs that supports several (possibly different) description logics, but the results presented are easily adaptable to other existing frameworks such as multi-context systems.

[10]Computing Repairs from Active Integrity Constraints (with P. Engrácia, G. Gaspar and I. Nunes)
in H. Wang and R. Banach (eds.), 2013 International Symposium on Theoretical Aspects of Software Engineering (TASE 2013), pages 183-190. IEEE, July 2013.
DOI 10.1109/TASE.2013.32

Abstract. Repairing an inconsistent knowledge base is a well-known problem for which several solutions have been proposed and implemented in the past. In this paper, we start by looking at databases with active integrity constraints – consistency requirements that also indicate how the database should be updated when they are not met – as introduced by Caroprese et al. We show that the different kinds of repairs considered by those authors can be effectively computed by searching for leaves of specific kinds of trees. Although these computations are in general not very efficient (deciding the existence of a repair for a given database with active integrity constraints is NP-complete), on average the algorithms we present make significant reductions on the number of nodes in the search tree. Finally, these algorithms also give an operational characterization of different kinds of repairs that can be used when we extend the concept of active integrity constraints to the more general setting of knowledge bases.

[9]Behavioural Theory at Work: Program Transformations in a Service-Centred Calculus (with I. Lanese, F. Martins, A. Ravara, and V. Vasconcelos), © Springer
in G. Barthe and F. de Boer (eds.), Proceedings of the 10th IFIP International Conference on Formal Methods for Open Object-based Distributed Systems (FMOODS'08), LNCS 5051:59-77. Springer, May 2008.
DOI 10.1007/978-3-540-68863-1_5

Abstract. We analyse the relationship between object-oriented modelling and session-based, service-oriented modelling, starting from a typical UML Sequence Diagram and providing a program transformation into a service-oriented model. We also provide a similar transformation from session-based specifications into request-response specifications. All transformations are specified in SSCC – a process calculus for modelling and analysing service-oriented systems – and proved correct with respect to a suitable form of behavioural equivalence (full weak bisimilarity). Since the equivalence is proved to be compositional, results remain valid in arbitrary contexts.

[8]Complete Axiomatization of Discrete-Measure Almost-Everywhere Quantification (with J. Rasga, A. Sernadas and C. Sernadas)
in Journal of Logic and Computation, 18(6):885-911. Oxford University Press, April 2008.
DOI 10.1093/logcom/exn014

Abstract. Following recent developments in the topic of generalized quantifiers, and also having in mind applications in the areas of security and artificial intelligence, a conservative enrichment of (two-sorted) first-order logic with almost-everywhere quantification is proposed. The completeness of the axiomatization against the measure-theoretic semantics is carried out using a variant of the Lindenbaum–Henkin technique. The independence of the axioms is analyzed, and the almost-everywhere quantifier is compared with related notions of generalized quantification.

[7]Heterogeneous Fibring of Deductive Systems via Abstract Proof Systems (with A. Sernadas and C. Sernadas)
in Logic Journal of the IGPL, 16(2):121-153. Oxford University Press, April 2008.
DOI 10.1093/jigpal/jzm057

Abstract. Homogeneous fibring is a meta-logical constructor that produces new logics by combining logics presented in the same way (e.g. both of them endowed with an Hilbert calculus). Heterogeneous fibring (e.g. one of the logics is presented by an Hilbert calculus and the other by a sequent calculus) is an open problem that we solve now. We start by considering consequence systems as providing a solution (a good one when fibring a logic presented by semantic means and another one presented in a deductive way). However consequence systems are not good when we want to obtain as the result of fibring two deductive systems still a deductive system (where a notion of derivation appears in the fibring). The solution is to introduce the concept of (abstract) proof system. The fibring of proof systems is still a proof system and so we have that a derivation in the fibring is obtained from the derivations of the component. Some preservation results are discussed like compactness and semi-decidability.

[6]Reasoning about Probabilistic Sequential Programs (with R. Chadha, P. Mateus and A. Sernadas)
in Theoretical Computer Science, 379(1-2):142-165. Elsevier, June 2007.
DOI 10.1016/j.tcs.2007.02.040

Abstract. A complete and decidable Hoare-style calculus for iteration-free probabilistic sequential programs is presented using a state logic with truth-functional propositional (not arithmetical) connectives.

[5]A Large-Scale Experiment in Executing Extracted Programs (with P. Letouzey)
in J. Carette and W.M. Farmer (eds.), Proceedings of the 12th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning (Calculemus 2005), ENTCS 151(1):75-191. Elsevier, 2006.
DOI 10.1016/j.entcs.2005.11.024

Abstract. It is a well-known fact that algorithms are often hidden inside mathematical proofs. If these proofs are formalized inside a proof assistant, then a mechanism called extraction can generate the corresponding programs automatically. Previous work has focused on the dificulties in obtaining a program from a formalization of the Fundamental Theorem of Algebra inside the Coq proof assistant. In theory, this program allows one to compute approximations of roots of polynomials. However, as we show in this work, there is currently a big gap between theory and practice. We study the complexity of the extracted program and analyze the reasons of its inefficiency, showing that this is a direct consequence of the approach used throughout the formalization.

Awarded best paper in the proceedings of CALCULEMUS 2005

[4]C-CoRN, the Constructive Coq Repository at Nijmegen (with H. Geuvers and F. Wiedijk), © Springer
in A. Asperti, G. Bancerek and A. Trybulec (eds.), Mathematical Knowledge Management, Third International Conference, MKM 2004, LNCS 3119:88-103. Springer, September 2004.
DOI 10.1007/978-3-540-27818-4_7

Abstract. We present C-CoRN, the Constructive Coq Repository at Nijmegen. It consists of a library of constructive algebra and analysis, formalized in the theorem prover Coq. In this paper we explain the structure, the contents and the use of the library. Moreover we discuss the motivation and the (possible) applications of such a library.

[3]Hierarchical Reflection (with F. Wiedijk), © Springer
in K. Slind, A. Bunker and G. Gopalakrishnan (eds.), Theorem Proving in Higher Order Logics (17th International Conference, TPHOLs 2004), LNCS 3223:66-81. Springer, September 2004.
DOI 10.1007/978-3-540-30142-4_5

Abstract. The technique of reflection is a way to automate proof construction in type theoretical proof assistants. Reflection is based on the definition of a type of syntactic expressions that gets interpreted in the domain of discourse. By allowing the interpretation function to be partial or even a relation one gets a more general method known as "partial reflection". In this paper we show how one can take advantage of the partiality of the interpretation to uniformly define a family of tactics for equational reasoning that will work in different algebraic structures. The tactics then follow the hierarchy of those algebraic structures in a natural way.

[2]Program Extraction from Large Proof Developments (with B. Spitters), © Springer
in D. Basin and B. Wolff (eds.), Theorem Proving in Higher Order Logics (16th International Conference, TPHOLs 2003), LNCS 2758:205-220. Springer, September 2003.
DOI 10.1007/10930755_14.

Abstract. It is well known that mathematical proofs often contain (abstract) algorithms, but although these algorithms can be understood by a human, it still takes a lot of time and effort to implement these algorithms on a computer; moreover, one runs the risk of making mistakes in the process.
From a fully formalized constructive proof one can automatically obtain a computer implementation of such an algorithm together with a proof that the program is correct. As an example we consider the fundamental theorem of algebra which states that every non-constant polynomial has a root. This theorem has been fully formalized in the Coq proof assistant. Unfortunately, when we first tried to extract a program, the computer ran out of resources.
We will discuss how we used logical techniques to make it possible to extract a feasible program. This example is used as a motivation for a broader perspective on how the formalization of mathematics should be done with program extraction in mind.

[1]A Constructive Formalization of the Fundamental Theorem of Calculus, © Springer
in H. Geuvers and F. Wiedijk (eds.), Types 2002, Proceedings of the workshop Types for Proof and Programs, LNCS 2646:108-126. Springer, April 2003.
DOI 10.1007/3-540-39185-1_7

Abstract. We have finished a constructive formalization in the theorem prover Coq of the Fundamental Theorem of Calculus, which states that differentiation and integration are inverse processes. In this formalization, we have closely followed Bishop's work [1]. In this paper, we describe the formalization in some detail, focusing on how some of Bishop's original proofs had to be refined, adapted or redone from scratch.
[1] Bishop, E., Foundations of Constructive Analysis, McGraw-Hill Book Company, 1967.

Other Publications with Refereeing

[10]A Formalisation of Approximation Fixpoint Theory (extended abstract, with B. Bogaerts)
in H. Basold (ed.), TYPES 2021 (Abstracts), Leiden, 2021.

Abstract. Extended abstract.

[9]Choreographies in Coq (extended abstract, with F. Montesi and M. Peressotti)
in M. Bezem (ed.), TYPES 2019 (Abstracts), Oslo, 2019.

Abstract. Extended abstract.

[8]The Boolean Pythagorean Triples Problem in Coq (extended abstract, with J. Marques-Silva and P. Schneider-Kamp)
in A. Kaposi (ed.), TYPES 2017 (Abstracts), pages 47-48, Budapest, 2017.

Abstract. Extended abstract.

[7]A Core Model for Choreographic Programming (with F. Montesi)
in R. Koshravi and O. Kouchnarenko (eds.), FACS 2016 (Pre-proceedings), October 2016.

Abstract. Early version of [35].

[6]Foundations of Choreographies (with F. Montesi)
in S. Gay and A. Ravara (eds.), BETTY 2016 (Proceedings), Lisbon, 2016.

Abstract. Extended abstract.

[5]Applying Sorting Networks to Synthesize Optimized Sorting Libraries (with M. Codish, M. Nebel and P. Schneider-Kamp)
in LOPSTR 2015 (Informal Proceedings), 2015.

Abstract. Early version of [24].

[4]A Formalized Checker for Size-Optimal Sorting Networks (extended abstract, with P. Schneider-Kamp)
in T. Uustalu (ed.), TYPES 2015 (Abstracts), pages 42-43, Tallinn, 2015.

Abstract. Extended abstract.

[3]Tighter integration in dl-programs (with P. Engrácia, G. Gaspar, R. Henriques, I. Nunes and D. Santos)
in J. Cachopo, B. Sousa Santos (eds.) INForum 2013, Atas do 5º Simpósio de Informática, pages 457-468, Évora, 2013.

Abstract. We introduce a mechanism called lifting to share predicates between the two components of a dl-program, integrating them in a tighter way. Using lifting, one can reason about the predicates being shared both via the description logic knowledge base and via Datalog-style rules, and the deductions one makes are automatically reflected globally on both components. This is a capability not directly present in dl-programs, since changes to the knowledge base only affect the queries where they occur. We show that lifting has nice theoretical properties, making it suitable for modular design of dl-programs. Furthermore, dl-program processors can easily incorporate lifting as a new operator, and we have extended dlvhex to work with dl-programs with lifting.

[2]Towards Automation of Real Analysis in Coq (extended abstract) (poster )
in J. Zimmer and C. Benzmüller (eds.), CALCULEMUS Autumn School 2002: Student Poster Abstracts, SEKI Report, Saarbrücken, 2002.

Abstract. Extended abstract (see poster).

[1]Formalizing Real Calculus in Coq
in V. Carreño, C. Muñoz and S. Tahar (eds.), Theorem Proving in Higher Order Logics, pages 158-166, NASA Conference Proceedings, Hampton VA, 2002.

Abstract. We have finished a constructive formalization in the theorem prover Coq of the Fundamental Theorem of Calculus, which states that differentiation and integration are inverse processes. This formalization is built upon the library of constructive algebra created in the FTA (Fundamental Theorem of Algebra) project, which is extended with results about the real numbers, namely about (power) series.
Two important issues that arose in this formalization and which will be discussed in this paper are partial functions (different ways of dealing with this concept and the advantages of each different approach) and the high level tactics that were developed in parallel with the formalization (which automate several routine procedures involving results about real-valued functions).

Technical Reports

[8]Information Flow within Relational Multi-context Systems (with G. Gaspar and I. Nunes),
Technical Report 2014;03, Faculdade de Ciências da Universidade de Lisboa, September 2014.

[7]Viewing dl-programs as multi-context systems (with R. Henriques and I. Nunes)
Technical Report 2013;05, Faculdade de Ciências da Universidade de Lisboa, April 2013.

Abstract. The combination of logic programs and description logic knowledge bases has been a fertile topic of research in the last years, with the proposal of several different systems that achieve this goal. In this paper, we look at two of these mechanisms, dl-programs and multi-context systems, which address different aspects of this combination, and include different, incomparable programming constructs. Despite this, we show that every dl-program can be transformed into a multi-context system in such a way that the different semantics for each paradigm are naturally related. As a consequence, many useful constructions developed within the framework of dl-programs may be automatically translated to equivalent constructions in the setting of multi-context systems.

[6]Patterns for Programming in the Semantic Web (with I. Nunes and G. Gaspar)
Technical Report 2012;06, Faculdade de Ciências da Universidade de Lisboa, October 2012.

Abstract. Originally proposed in the mid-90s, design patterns for software development played a key role in object-oriented programming not only in increasing software quality, but also by giving a better understanding of the power and limitations of this paradigm. Since then, several authors have endorsed a similar task for other programming paradigms, in the hope of achieving similar benefits.
In this paper we discuss design patterns for the Semantic Web, giving new insights on how existing programming frameworks can be used in a systematic way to design large-scale systems. The common denominator between these frameworks is the combination between different reasoning systems, namely description logics and logic programming. Therefore, we chose to work in a generalization of dl-programs that supports several (possibly different) description logics, expecting that our results will be easily adapted to other existing frameworks such as multi-context systems. This study also suggests new constructs to enforce legibility and internal structure of logic-based Semantic Web programs.

[5]Achieving tightness in dl-programs (with P. Engrácia, G. Gaspar and I. Nunes)
Technical Report 2012;03, Faculdade de Ciências da Universidade de Lisboa, July 2012.

Abstract. In the field of the combination between description logics and rule-based reasoning systems, dl-programs have proved to be a very successful mechanism. One of their recognized shortcomings, however, is their lack of full tightness: the language constructs that feed data from the logic program have a local effect, leaving the knowledge base essentially unchanged throughout. In this paper, we present a construction that we call lifting, which allows predicates to be fully shared between the two components of a dl-program in a systematic way, and show how lifting can be used to provide intuitive solutions to a number of everyday reasoning problems involving the verification of integrity constraints and the implementation of default rules. This construction preserves consistency of the underlying knowledge base and complexity of the overall system. Furthermore, the resulting semantics of default rules has a natural interpretation under the original Reiter semantics.

[4]Bisimulations in SSCC (with I. Lanese, F. Martins, A. Ravara, V. Vasconcelos)
Technical Report 07-37, Faculdade de Ciências da Universidade de Lisboa, December 2007.

Abstract. This report studies different definitions of bisimulation within the Stream-Based Service-Centered Calculus (SSCC) and shows that both strong and weak ground bisimulation are non-input congruences.

[3]The Essence of Proofs when Fibring Sequent Calculi (with C. Sernadas)
Technical Report, CLC, Lisbon, Portugal, 2005

Abstract. Extended abstract.

[2]Equational Reasoning in Algebraic Structures: a Complete Tactic (with F. Wiedijk)
Research Report NIII-R0431, NIII, University of Nijmegen, July 2004.

Abstract. We present rational, a Coq tactic for equational reasoning in abelian groups, commutative rings, and fields. We give an mathematical description of the method that this tactic uses, which abstracts from Coq specifics.
We prove that the method that rational uses is correct, and that it is complete for groups and rings. Completeness means that the method succeeds in proving an equality if and only if that equality is provable from the the group/ring axioms. Finally we characterize in what way our method is incomplete for fields.

[1]C-CoRN: the Constructive Coq Repository at Nijmegen (with H. Geuvers and F. Wiedijk)
in Dutch Proof Tools Day 2004 (Program + Proceedings), Research Report NIII-R0429, NIII, University of Nijmegen, June 2004.

Abstract. Early version of [4].

Theses

[2]Constructive Real Analysis: a Type-Theoretical Formalization and Applications
PhD thesis, University of Nijmegen, June 2004.

Abstract. A description of the whys and hows of the construction of a library of formalized mathematics, addressing among others issues of representation of concepts, automation, differences between the informal and formal proofs and applications.

[1]Lambda Calculus and Beyond
Diploma thesis, Instituto Superior Técnico, Lisbon, June 2001.

Abstract.A survey of Lambda Calculus and related questions, including computational completion of combinatory algebras, Pure Type Systems and the Curry–Howard isomorphism.

Books (editor)

[4]Números, cirurgias e nós de gravata: 10 anos de Seminário Diagonal no IST (with J.P. Boavida, R. Carpentier, E. Grifo, P. Gonçalves, D. Henriques and A.R. Pires)
Lisbon, 2012.

[3]Seminário Diagonal–Proceedings IST, III (with A. Cannas da Silva, N. Freitas, J.D. Silva and A. Vasconcelos)
Lisbon, 2007.

[2]Seminário Diagonal–Proceedings IST, II (with A. Cannas da Silva, R. Gonçalves, J. Pimentel Nunes, A.R. Pires, T. Reis, P.M. Resende and J. Silva)
Lisbon, 2005.

[1]Seminário Diagonal–Proceedings IST 2000-01 (with J.P. Boavida, A. Cannas da Silva, J. Fachada and P. Resende)
Lisbon, 2001.

Other Publications

[2]Uma Forma Diferente de Fazer Contas
in J.P. Boavida, R. Carpentier, L. Cruz-Filipe, P. Gonçalves, E. Grifo, D. Henriques and A.R. Pires (eds.), Números, cirurgias e nós de gravata: 10 anos de Seminário Diagonal no IST, Lisbon, 2012.

Abstract. Para muitos matemáticos, a Matemática é fundamentalmente um jogo. Neste artigo, apresentamos exactamente isso – apenas um jogo, com regras extremamente simples, que se descobre afinal ser um modelo teórico do funcionamento de um computador tão válido como qualquer outro.

[1]Habilidades com Somatórios
in J.P. Boavida, A. Cannas da Silva, L. Cruz-Filipe, J. Fachada and P. Resende (eds.), Seminário Diagonal–Proceedings IST 2000-01, Lisbon, 2001.

Abstract. Alguns quebra-cabeças relativamente simples criam por vezes a necessidade de calcular somas pouco atraentes. Neste apontamento introduzem-se técnicas elegantes que permitem resolver alguns somatórios sem esforço recorrendo, nomeadamente, à introdução de uma notação diferente da habitual.

Unpublished notes

[9]Active Integrity Constraints and Operational Aspects of the Problem of Database Repair (with P. Engrácia, G. Gaspar, I. Nunes and P. Schneider-Kamp), 2018.

Abstract. Repairing an inconsistent database is a well-known problem for which several partial approaches have been proposed and implemented in the past. One of the existing proposals uses active integrity constraints (AICs), which are consistency requirements that also allow one to restrict the possible ways to repair inconsistencies. The typical semantics for AICs is declarative, and thus suggests no algorithms to compute repairs.
In this article, we show how AICs may be used directly to repair inconsistent databases in an efficient way. First, we introduce notions of independence and precedence on AICs that allow the search for repairs to be, respectively, parallelized and sequentialized. Afterwards, we present an operational semantics and show that the different kinds of repairs for AICs can be effectively computed as leaves of specific kinds of trees. We show that this operational semantics is complete when existence of a repair is an NP-complete problem. Finally we discuss the applicability of these techniques and results to integrity constraints in general.

[8]On Asynchrony and Choreographies (with F. Montesi), 2018.

Abstract. Choreographic Programming is a paradigm for the development of concurrent software, where deadlocks are prevented syntactically and then correct-by-construction implementations in process models are mechanically generated. The formal semantics of choreography languages are typically based on synchronous communications, in order to achieve a simpler theory. However, many real-world systems have asynchronous communications. Previous attempts at enriching choreographies with asynchrony rely on ad-hoc constructions, whose adequacy is only argued informally.
In this work, we present a systematic study of asynchronous communications in choreographies. First, we discuss and formalise the properties that an asynchronous semantics for choreographies should have. Then, we explore how out-of-order execution, previously used in choreographies for modelling concurrency, can be used to endow choreographies with an asynchronous semantics that satisfies our properties. Our development yields a pleasant correspondence with FIFO-based asynchronous messaging, modelled in a process calculus. Finally, we investigate the expressivity of choreography languages with respect to asynchrony. Specifically, we find out that choreography languages equipped with process spawning and name mobility primitives are expressive enough to program asynchronous behaviour over a simple synchronous semantics.

[7]Procedural Choreographic Programming (with F. Montesi), 2017.

Abstract. Choreographic Programming is an emerging paradigm for correct-by-construction concurrent programming based on message passing. Models based on choreographic programming have been successfully developed for different settings where concurrent programming is challenging, including service-oriented computing and cyber-physical systems. However, the general applicability of the paradigm is limited by the current lack of support for reusable procedures, which hinders modularity.
We propose Procedural Choreographies (PC), a choreographic language model with full procedural abstraction. PC includes unbounded process creation and name mobility, yielding a powerful framework for writing correct concurrent algorithms that can be compiled into a process calculus. This expressivity requires a typing discipline to ensure that processes are properly connected when enacting procedures. Connections may form networks of arbitrary graph structures. We develop a formal synthesis procedure that, given a program in PC, generates a correct-by-construction concurrent implementation in terms of a process calculus. We illustrate the expressivity of PC with a series of examples, including parallel streams and parallel computation based on pipelining.

[6]Connectors meet Choreographies (with F. Arbab, S. Jongmans and F. Montesi), 2016.

Abstract. Choreographic Programming is a paradigm for developing concurrent programs that are deadlock-free by construction, by syntactically disallowing mismatched I/O and then synthesising process implementations automatically. Most choreography models assume that all communication occurs synchronously between two parties. This has been relaxed in some settings, allowing for example asynchronous communications, many-to-one, or one-to-many. However, these extensions are hardcoded in the syntax and semantics of each particular model.
In this work, we present Cho-Reo-graphies (CR), a model where choreographies are parametric in the (Reo) connectors through which parties communicate. CR is the first choreography model where different communication semantics (e.g., synchronous and asynchronous) can freely be mixed in the same choreography. We prove that if a choreography respects the rules of the connectors that it uses, then the process implementation that we can synthesise from it enjoys deadlock freedom.

[5]When Six Gates are Not Enough (with M. Codish, M. Frank and P. Schneider-Kamp), 2015.

Abstract. We study the topology of Boolean circuits and apply the pigeonhole principle to show that there must exist Boolean functions on 7 inputs with a multiplicative complexity of at least 7, i.e., that cannot be computed with only 6 multiplications in the Galois field with two elements. Focusing on topology also enables to improve other lower bounds on multiplicative complexity.

[4]Cut-elimination theorem for second-order logic (with F. Ferreira)
Unpublished note, August 2013.

Abstract. This note contains the full proof of the cut-elimination theorem in [13] above.

[3]The Automotive Case Study in the Sensoria Core Calculi (with F. Martins and V. Vasconcelos)
Unpublished note, June 2007.

[2]Sequent Calculi Based on Derivations (with C. Sernadas)
Unpublished note, 2005.

Abstract. Fibring is a meta-logical constructor that combines two given logics and produces a new one. In particular, the fibring of two sequent calculi is obtained by combining the languages of both calculi and taking all rules allowed in either calculus. By their own nature, proofs in the fibring have no relationship to proofs in the components, so that these are essentially different objects. In this paper, we propose a novel definition of fibring of two sequent calculi that takes the notion of derivation as primitive. Using this construction, we show that a proof in the fibring is essentially a finite set of proofs in the components structured in a meaningful way. We also use this novel definition to show that fibring preserves cut elimination and decidability.

[1]A Decision Procedure for Equational Reasoning in Commutative Algebraic Structures (with F. Wiedijk)
Unpublished note, October 2004.

Abstract. We present a decision procedure for equational reasoning in abelian groups, commutative rings and fields that checks whether a given equality can be proven from the axioms of these structures. This has been implemented as a tactic in Coq; here we give a mathematical description of the decision procedure that abstracts from Coq specifics, making the work in principle adaptable to other theorem provers.
Within Coq we prove that this decision procedure is correct. On the meta-level we analyse its completeness, showing that it is complete for groups and rings in the sense that the tactic succeeds in finding a proof of an equality if and only if that equality is provable from the group/ring axioms without any hypotheses. Finally we characterize in what way our method is incomplete for fields.

	Home	Research	Teaching	Personal
	Suggestions or comments: lcfilipe thingy gmail.com