Talks

This is a detailed archive of my talks in reverse chronological order. For most of these you can download a pdf version of the slides used in the presentation – exceptions occur when I simply used an old-fashioned blackboard. The older ones were generated from other formats, so they are missing the animations. Most of the abstracts and slides are in English. Exceptions are when they are in Portuguese :-) The title should give some clues as to which is the case.

Presentations that refer to work that has been published include a link (next to the title) to the relevant article in my publication list.

Formalising choreographic programming paper
8.Sep.2021 • ICTAC 2021, Nur-Sultan, Kazakhstan pdf

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.

Formalizing choreographic programming
12.Jul.2021 • VEST 2021, online workshop pdf
Formalizing choreographies in Coq
20.Nov.2020 • Concurrency and Logic seminar, University of Southern Denmark, Denmark pdf

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.
We present a formalisation in Coq of the theory of a minimal choreography language. In this formalisation we define the syntax and semantics of this language and its associated process calculus, prove that choreography compilation for this language is sound and complete, and show that the choreography language is Turing-complete. To the best of our knowledge, this is the first formalisation of choreography compilation for a nontrivial language supporting recursion.

Formalising a Turing-complete choreographic language in Coq paper
1.Jul.2021 • ITP 2021, Rome, Italy pdf

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.

A formalisation of approximation fixpoint theory paper
14.Jun.2021 • TYPES 2021, Leiden, The Netherlands pdf

Abstract. Preliminary report on a formalization of approximation fixpoint theory in the theorem prover Coq.

Can computers prove theorems?
31.Mai.2021 • Mathematical Logic Webinar, FCUL, Lisboa, Portugal pdf

Abstract. The proof of the four-color theorem in 1976 is usually referenced as the birth of computer-assisted mathematical proofs, although some earlier examples exist. Since then, computers have slowly started working their way into mathematicians' toolboxes; and the relevance of computers for mathematical proofs was confirmed with the inclusion of a panel discussion on the topic at ICM 2018.
In this talk we discuss the logical foundations of computer proofs and what it means to say that a theorem has been proved with the help of a computer. We cover some recent examples from combinatorics and number theory, and discuss ongoing work around the topic of session types.

Choreography extraction
13.Nov.2020 • Concurrency and Logic seminar, University of Southern Denmark, Denmark pdf
The Paths to Choreography Extraction paper
27.Apr.2017 • FoSSaCS 2017, Uppsala, Sweden pdf

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.

Certificeret software og explainable AI
18.Jun.2020 • Forsvars roadshow, Odense, Denmark pdf

Abstract. Small presentation on certified software and explainable AI.

Hypothetical answers to continuous queries on data streams paper
9.Feb.2020 • AAAI-20, New York, NY, USA pdf
Hypothetical answers to continuous queries on data streams paper
30.Jan.2020 • Days in Logic 2020, FCUL, Lisboa, Portugal pdf
Hypothetical answers to continuous queries on data streams paper
17.Jan.2020 • Concurrency and Logic seminar, University of Southern Denmark, Denmark pdf

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 talk 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.

Formalizing a Turing-complete choreography calculus in Coq paper
13.Jun.2019 • TYPES 2019, Oslo, Norway pdf

Abstract. Preliminary report on a formalization of a choreography language in the theorem prover Coq.

Some thoughts on machine-assisted proofs paper
7.Aug.2018 • ICM 2018, Rio de Janeiro, Brazil pdf

Abstract. Invited contribution to the expert panel on Machine-Assisted Proofs held in the International Congress of Mathematicians.

How to Get More Out of Your Oracles paper
28.Sep.2017 • ITP 2017, Brasília, Brazil pdf
Formal Verification of Very Large Proofs in Coq
7.Sep.2017 • PART Workshop 2017, Technical University of Denmark, Lyngy, Denmark pdf

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.

The Boolean Pythagorean Triples Problem in Coq paper
21.Jul.2017 • Logic and Computation Seminar, Instituto Superior Técnico, Lisboa, Portugal pdf
1.Jun.2017 • TYPES 2017, Budapest, Hungary pdf

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.

On Asynchrony and Choreographies paper
21.Jun.2017 • ICE 2017, Neuchâtel, Switzerland pdf

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.

Procedural Choreographic Programming paper
20.Jun.2017 • FORTE 2017, Neuchâtel, Switzerland pdf

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.

Formally Proving the Boolean Pythagorean Triples Conjecture paper
12.May.2017 • LPAR-21, Maún, Botswana pdf

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.

Connectors Meet Choreographies paper
31.Mar.2017 • Talks@DI, Department of Informatics, FCUL, Lisboa, Portugal pdf

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.

Foundational Questions in Choreographic Programming
25.Nov.2016 • Logic and Computation Seminar, Instituto Superior Técnico, Lisboa, Portugal pdf

Abstract. Choreographies are widely used for the specification of concurrent and distributed software architectures. In previous work, we proposed Core Choreographies (CC), a model for investigating foundational questions in choreography calculi. In this talk, we discuss two such questions: asynchrony and behaviour extraction.
Asynchronous communications are ubiquitous in real-world systems, and we show how it can be modeled either by endowing CC with a different semantics or by minimally extending its syntax and implementing message queues. Since CC is a core model, these constructions can be generalized to most choreography languages.
Extraction concerns the issue of deciding whether the behaviour of a given process network can be expressed as a choreography, and if possible finding this choreography. In general, these questions are undecidable; we show that in CC we can find algorithms to answer them.

Active Integrity Constraints for Multi-Context Systems paper
23.Nov.2016 • EKAW 2016, Bologna, Italy pdf

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.

A Core Model for Choreographic Programming paper
21.Oct.2016 • FACS 2016, Besançon, France pdf
A Turing-Complete Choreography Calculus
9.Sep.2016 • ACBD Seminar, University of Glasgow, Scotland pdf
23.Abr.2016 • Amílcar Sernadas Festschrift, Lisbon, Portugal pdf

Abstract. We investigate the foundations of Choreographic Programming, a paradigm for writing concurrent programs that are deadlock free by construction, guided by the notion of computation. We start by introducing Minimal Choreographies (MC), a language that includes only the essential primitives of the paradigm. MC is minimal with respect to Turing completeness: it implements all computable functions, and restricting its syntax breaks this property. Our methodology yields a natural notion of computation for choreographies, which can be used to generate concurrent implementations of independent computations automatically. Finally, we show that a Turing complete fragment of MC can be correctly projected to a process calculus (synthesis), which is thus both deadlock free and Turing complete.

Grounded Fixpoints and Active Integrity Constraints paper
18.Oct.2016 • ICLP 2016, New York, NY, USA pdf
21.Dec.2015 • LabMAg Seminar, Department of Informatics, FCUL, Lisboa, Portugal

Abstract. The problem of repairing a database that is inconsistent with respect to a given set of integrity constraints has been intensively studied during the last fifty years. One important aspect is choosing among several possible candidate repairs, and several authors have proposed different criteria to achieve this task.
In this talk, we address this question using ideas from algebraic fixpoint theory. We show how database repairs can be modelled as fixpoints of particular operators on databases. The recently introduced notion of grounded fixpoint then induces a corresponding notion of grounded database repair that captures several natural intuitions. Focusing in particular on the approach of active integrity constraints, we show that grounded repairs lie between the well-studied semantics of founded and justified repairs, providing a middle-ground that avoids the unintuitive examples of both definitions.
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.

Foundations of Choreographies paper
6.Oct.2016 • BETTY Meeting, Lisbon, Portugal pdf

Abstract. Recent advances in choreographic programming.

Choreographies in Practice paper
7.Jun.2016 • FORTE 2016, Heraklion, Greece pdf

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.

Integrity Constraints for General-Purpose Knowledge Bases paper
8.Mar.2016 • FoIKS 2016, Linz, Austria pdf

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 talk 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.

A Formalized Checker for Size-Optimal Sorting Networks paper
27.Aug.2015 • ITP 2015, Nanjing, China pdf

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 talk, 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.

A Turing-Complete Choreography Calculus paper
21.Jul.2015 • LabMAg Seminar, Department of Informatics, FCUL, Lisboa, Portugal pdf

Abstract. Choreographic Programming is a programming paradigm for building concurrent software that is deadlock-free by construction, by disallowing mismatched I/O operations in the language used to write programs (called choreographies). Previous models for choreographic programming are either trivially Turing complete, because they include arbitrary local computations at each process, or trivially Turing incomplete, e.g., because termination is decidable.
In this work, we explore the core expressivity of choreographies, by introducing a minimal language (AC) with restricted local computation (zero, successor, and equality). AC is Turing complete purely by virtue of the communication structures that can be written in it. We show that a Turing-complete fragment of AC can be correctly projected to an actor-like process calculus (AP), thus identifying a process language that is both deadlock-free and Turing-complete. By embedding AC into CC, a standard model for choreographies based on sessions, we also characterise a Turing-complete fragment of CC, showing that the local computation primitives found in previous works do not add expressive power. As a corollary, we identify a fragment of the session-based π-calculus that is both deadlock-free and Turing complete.

Optimizing a Certified Proof Checker for a Large-Scale Computer-Generated Proof paper
16.Jul.2015 • CICM 2015, Washington, DC, USA pdf

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 talk, 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.

A Formalized Checker for Size-Optimal Sorting Networks paper
20.May.2015 • TYPES 2015, Tallinn, Estonia pdf

Abstract. In 2014 we first proved that 25 comparisons are optimal for sorting 9 inputs. In this talk, we present a formal proof of this result, obtained by using the results from the original computer-assisted proof as an oracle to a checker extracted from a Coq formalization. Besides the result itself, the techniques we used help us understand how to deal with computer-assisted proofs involving amounts of witnesses previously considered prohibitive.

Advances in Sorting Networks
28.Apr.2015 • Brouwer Seminar, University of Nijmegen, The Netherlands pdf

Abstract. Sorting networks are a very simple model of data-independent sorting algorithms, suitable for implementation in hardware. Proving optimality of a sorting network, whether in terms of number of necessary gates or execution steps, remains however a daunting task, as it requires showing that no smaller arrangements of gates can sort all inputs. Due to the huge combinatorial explosion, after the initial results obtained in the 60s there was almost no advance in this field for nearly fifty years.
In this talk, I will introduce the topic and the problems we are most interested in addressing, and show how a novel combination of new theoretical insights and advances in computer-science has led to a number of computer-assisted proofs of new results about sorting networks during the last two years.

Sorting Networks: the End Game paper
13.Apr.2015 • LabMAg Seminar, Department of Informatics, FCUL, Lisboa, Portugal pdf
5.Mar.2015 • LATA 2015, Nice, France pdf
14.Nov.2014 • ARCO Workshop, Copenhagen, Denmark pdf

Abstract. Sorting networks are a very simple model of data-independent sorting algorithms, suitable for implementation in hardware. Proving optimality of a sorting network, whether in terms of necessary gates or in terms of execution steps, remains however a daunting task, as it requires showing that no smaller arrangements of gates can sort all outputs. Due to the huge combinatorial explosion, this problem has only been settled for inputs of small size, and all current results rely on breaking symmetries in the first comparisons made. In this talk, we discuss the properties of the last comparators in a sorting network, and show how these results help both towards improving the best-known sorting networks or proving their optimality.

Information Flow within Relational Multi-context Systems paper
26.Nov.2014 • EKAW 2014, Linköping, Sweden pdf

Abstract. Multi-context systems (MCSs) are an important framework for heterogeneous combinations of systems within the Semantic Web. In this talk, we propose generic constructions to achieve specific forms of interaction in a principled way, and systematize 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.

Twenty-five Comparators is Optimal when Sorting Nine Inputs paper
10.Nov.2014 • ICTAI 2014, Limassol, Cyprus pdf
Proofs for Minimality of Sorting Networks by Logic Programming
17.Jul.2014 • CICLOPS-WLPE Workshop, Vienna, Austria (with P. Schneider-Kamp) pdf
Minimal-Size Sorting Networks for 9 and 10 Inputs
11.Jul.2014 • Logic and Computation Seminar, Instituto Superior Técnico, Lisboa, Portugal pdf
9.Jul.2014 • LabMAg Seminar, Department of Informatics, FCUL, Lisboa, Portugal pdf
18.Jun.2014 • University of Roskilde, Denmark pdf

Abstract. We present 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 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 entire implementation is written in SWI-Prolog and was run on a cluster of 12 nodes with 12 cores each able to run concurrently a total of 288 threads, making extensive use of both SWI-Prolog's built-in concurrency/3. The search space of 2.2×1037 comparator networks was exhausted after just under 10 days of computation. This shows the ability of logic programming to provide a scalable parallel implementation while at the same time instilling a high level of trust in the correctness of the proof.

The Quest for Optimal Sorting Networks paper
23.Sep.2014 • SYNASC 2014, Timisoara, Romania pdf
19.Aug.2014 • IMADA Colloquium, University of Southern Denmark pdf
Two-Layer Filters for Sorting Networks
16.Abr.2014 • LabMAg Seminar, Department of Informatics, FCUL, Lisboa, Portugal pdf

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. In this talk we revisit the problem of generating two-layer prefixes modulo symmetries. We provide an improved notion of symmetry and a novel technique based on regular languages and graph isomorphism 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.

Efficient Repair of Inconsistent Databases paper
5.Mar.2014 • FoIKS 2014, Bordeaux, France pdf
Optimizing the Search for Repairs from Active Integrity Constraints
18.Sep.2013 • LabMAg Seminar, Department of Informatics, FCUL, Lisboa, Portugal pdf
13.Sep.2013 • IMADA Colloquium, University of Southern Denmark pdf

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 ΣP2-complete problem, depending on the type of repairs one has in mind. In order to make the search for repairs more efficient, we introduce two different relations on AICs: an equivalence relation of independence, allowing the search to be parallellized among the equivalence classes, and a precedence relation, inducing a stratification that allows repairs to be built progressively.

Description Logics, Rules and Multi-Context Systems paper
18.Dec.2013 • LPAR-19, Stellenbosch, South Africa pdf
6.Dec.2013 • LabMAg Seminar, Department of Informatics, FCUL, Lisboa, Portugal pdf

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 talk, we look at two of these formalisms, 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.

Computing Repairs from Active Integrity Constraints paper
3.Jul.2013 • TASE 2013, University of Birmingham, UK pdf
25.Jun.2013 • LabMAg Seminar, Department of Informatics, FCUL, Lisboa, Portugal pdf

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 talk, 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.

Services: when specification meets implementation
7.Apr.2009 • Brouwer Institute Seminar Series, Radboud Universiteit Nijmegen, The Netherlands pdf
1.Apr.2009 • GLOSS Seminar, Department of Informatics, FCUL, Lisboa, Portugal pdf

Abstract. Within the Sensoria project, several approaches have been proposed to the design, modelling and implementation of service-oriented systems. These approaches stem from different motivations, different perspectives and different levels of abstraction, and have different goals in mind; however, the object of their study is the same, and as such they often share several non-trivial common features below the surface.
This talk focuses on two languages and the concepts they share. On a higher level, SRML is a modelling language aimed at supporting the more abstract levels of design specification (“business modelling”). On a lower level, the Conversation Calculus models services as processes that can be analyzed using techniques from process calculus. We will show that these two approaches end up sharing a significant number of concepts, and establish a relationship between CC processes and SRML specifications that not only highlights these similarities, but also provides more powerful tools for analyzing and studying properties of these systems.

Reasoning about probabilistic sequential programs paper
3.Nov.2006 • Logic and Computation Seminar, Instituto Superior Técnico, Lisboa, Portugal pdf
19.Oct.2006 • Seminário de Lógica Matemática, Lisboa, Portugal pdf

Abstract. We introduce a simple programming language to develop iteration-free probabilistic sequential programs and develop a complete and decidable Hoare calculus for this programming language. In contrast to the usual approach, our state logic has truth-functional rather than arithmetical propositional connectives.

First-order logic with almost-everywhere quantification paper
2.Dez.2005 • Logic and Computation Seminar, Instituto Superior Técnico, Lisboa, Portugal

Abstract. Following recent developments in the topic of generalized quantifiers, and also having in mind subsequent applications to the area of cleistic logic, we propose a conservative enrichment of first-order logic with almost-everywhere quantification, endowed with measure-theoretic semantics.The completeness of the axiomatization we provide is carried out using a variant of the Lindenbaum-Henkin technique.The independence of the axioms is analysed, and the almost-everywhere quantifier is classified using the taxonomy proposed by Carnielli et al.

Execution of Extracted Programs paper
18.Jul.2005 • CALCULEMUS Workshop, Newcastle-upon-Tyne, United Kingdom pdf

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 difficulties 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.

The Essence of Proofs in Sequent Calculi paper
5.Oct.2005 • Brouwer Seminar, Radboud University of Nijmegen, Nijmegen, The Netherlands pdf
13.May.2005 • Logic and Computation Seminar, Instituto Superior Técnico, Lisboa, Portugal pdf

Abstract. Fibring is a technique for combining logics that has been extensively studied in the last decade. A simple way of fibring two sequent calculi is by combining the languages of both calculi and taking all rules allowed in either calculus. However, proofs in the fibring thus defined have no relationship to proofs in the original systems. In this talk, we propose a different definition of fibring of two sequent calculi where the notion of derivation is primitive and show that we obtain a system where proofs are essentially finite sets of proofs in the components structured in a meaningful way. As a consequence, we can show in a very easy way that fibring preserves cut elimination and decidability of the calculi.

Hierarchical Reflection paper
15.Sep.2004 • TPHOLs 2004, Park City, Utah, USA pdf
16.Feb.2004 • Brouwer Seminar, University of Nijmegen, The Netherlands pdf
16.Jan.2004 • Logic and Computation Seminar, Instituto Superior Técnico, Lisboa, Portugal pdf

Abstract. Reflection-based tactics are very useful in theorem proving. When doing reflection one defines a type of syntactic expressions that get interpreted in the domain of discourse. By allowing the interpretation function to be partial, one gets a more general method known as “partial reflection”. In this talk we show how partial reflection can be used to define a tactic for proving equalities in a field in such a way that it will also work in simpler algebraic structures, such as groups and rings.

Completeness of First-Order Logic with Partial Functions
6.Sep.2004 • Brouwer Seminar, Radboud University of Nijmegen, Nijmegen, The Netherlands pdf
23.Jul.2004 • Logic and Computation Seminar, Instituto Superior Técnico, Lisboa, Portugal pdf

Abstract. In most branches of mathematics, total functions are the exception rather than the rule. But representing partiality in formal systems like first-order logic (FOL) or type theory is quite tricky, since by their own nature these systems deal only with total objects.
With this in mind, Wiedijk and Zwanenburg introduced an extension of FOL where functions are allowed to be partial and showed that their system was equivalent to FOL with so-called “domain conditions”. In this talk we look at the model theory for their system, which has some unexpected differences from the model theory for FOL, and show that the equivalence they showed also holds at the semantic level. As a consequence, we obtain completess of this system.

C-CoRN: The Constructive Coq Repository at Nijmegen paper
9.Jul.2004 • Dutch Proof Tools Day, Nijmegen, The Netherlands pdf
22.Jan.2004 • Days in Logic, Braga, Portugal pdf

Abstract. At the University of Nijmegen, a large formalization of constructive mathematics has been developed in the theorem prover Coq. This formalization contains a library of constructive algebra and analysis, including results like the Fundamental Theorem of Algebra and the Fundamental Theorem of Calculus as well as the definition and basic properties of the elementary transcendental functions.
In this talk we will present this library. We will start by discussing why formalizing mathematics is relevant, and then give an overview of the structure and contents of the library together with the methodology that is used to ensure that it remains consistent and that it can be used by other people.
Finally some applications will be considered, with emphasis on program extraction. This will include a motivation of program extraction and presentation of what has been done within the framework of the Constructive Coq Repository at Nijmegen.

Constructive Real Analysis: a Type-Theoretical Formalization and Applications paper
15.Jun.2004 • Aula of the University of Nijmegen, The Netherlands pdf

Abstract. PhD defense.

Representação de provas em teoria de tipos
6.May.2004 • National Meeting of the Portuguese Mathematical Society, Porto, Portugal pdf

Abstract. O isomorfismo de Curry–Howard estabelece uma correspondência entre derivações numa lógica e termos numa teoria de tipos. A verificação do tipo de um termo é, para muitas teorias de tipos, não só um problema decidível como pode ser resolvido por algoritmos muito simples. Assim, os sistemas de tipos constituem um modo muito conveniente de representar e verificar demonstrações num computador.
Nesta apresentação discutir-se-á o potencial de uma tal representação, não só duma perspectiva teórica mas também ilustrando as suas possíveis aplicações.

A New Look at the Fundamental Theorem of Algebra
30.Apr.2004 • Seminário do Centro de Álgebra da Universidade de Lisboa, Portugal pdf
20.Jan.2004 • Centro de Matemática da Universidade de Coimbra, Portugal pdf

Abstract. In this talk we will explore one application of a constructive formalization of the Fundamental Theorem of Algebra. We begin by discussing the theoretical and practical interest of formalizing mathematics, before a constructive proof of the FTA is presented in detail. Then we look at the algorithm implicit in this proof to focus on the problem of extracting the corresponding computer program from a computer representation of the proof.

Formalizing Constructive Real Analysis in Type Theory paper
16.Mar.2004 • ZIC-colloquium, University of Eindhoven, The Netherlands pdf

Abstract. In this talk we present C-CoRN, the Constructive Coq Repository at Nijmegen. As its name suggests, C-CoRN is a library of formalized constructive mathematics developed in the theorem prover Coq. In what way and for what purposes such a library can be developed and used will be the main topics of the presentation.
One of the basic definitions in C-CoRN is that of partial function. We discuss and compare several different ways in which partial functions can be represented both in Coq and in other type theories. As an example of the use of this definition, we show how the usual functions of analysis (sine, exponential, logarithm) can be defined and used.
Another aspect of C-CoRN is automation of proofs. I explain how equational reasoning can be done without user intervention and show how this hugely simplifies proofs.
Finally, we pursue the possible applications of C-CoRN with an overview of program extraction and how, in theory, the formalization of the Fundamental Theorem of Algebra could be used to obtain a root-finding program. Unfortunately, as will be seen, the theory and the practice do not coincide.

Program Extraction from Large Proof Developments (II) paper
17.Oct.2003 • Theory of Computation Seminar, Instituto Superior Técnico, Lisboa, Portugal pdf
13.Oct.2003 • Grondslagen group seminar, University of Nijmegen, The Netherlands pdf

Abstract. It is well known that constructive proofs of mathematical statements implicitly contain an algorithm within them. However, actually obtaining a computer program from a formalized proof can be far from straightforward. In this talk, a constructive proof of the Fundamental Theorem of Algebra will be examined as a non trivial case study. The extracted program has many surprising properties, and it will be discussed how a careful look at this program can provide interesting insights on the process of formalization.

Program Extraction from Large Proof Developments paper
11.Sep.2003 • TPHOLs 2003, Rome, Italy pdf

Abstract. see the abstracts for “Program Extraction from Large Proof Developments (I)” and “Program Extraction from Large Proof Developments (II)”

Formalizing Mathematics in Coq: Applications
11.Jun.2003 • Fields Institute Summer School, Ottawa, Canada (student presentation)

Abstract. Brief overview of some problems arising from program extraction from a library of formalized mathematics in the theorem prover Coq.

C-CoRN: The Constructive Coq Repository at Nijmegen paper
30.Apr.2003 • TYPES 2003 Workshop, Torino, Italy pdf

Abstract. We will present C-CoRN, a documented library of constructive mathematics formalized in Coq, and maintained by the Foundations group of the Computer Science Department of the University of Nijmegen. In the talk we will first present the background motivations for this activity why formalize mathematics on a computer, why work constructively, why make a big library?) Then we will describe the setup of the repository and the way it is organised: the repository is “open” in the sense that people can download it and are invited to contribute to it. However, we only want to add contributions that obey certain standards, which we will describe in the talk.
Finally we will give an overview of the content of the repository as it is and the developments which we plan to do in the near future.

What do we want from a documentation tool?
24.Apr.2003 • Math in Coq Meeting, Orsay, France

Abstract. A manifest for a documentation system for C-CoRN (and Coq).

Program Extraction from Large Proof Developments (I) paper
28.Mar.2003 • Theory of Computation Seminar, Instituto Superior Técnico, Lisboa, Portugal pdf
19.Mar.2003 • Grondslagen group seminar, University of Nijmegen, The Netherlands pdf

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 this algorithm on a computer; moreover, one runs the risk of making mistakes in the process.
From a fully formalized constructive proof one can in theory automatically obtain a computer implementation of such an algorithm. As an example we consider the fundamental theorem of algebra; on the first attempts to extract a program from its formalization, the computer ran out of resources.
We will discuss how we used logical techniques 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.

Formalizing Real Calculus in Coq paper
19.Aug.2002 • Formalizing Continuous Mathematics 2002 (workshop in TPHOLs 2002), Hampton, VA, USA pdf

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 talk 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).

Towards the Automation of Proofs in Real Analysis
12.Jul.2002 • Theory of Computation Seminar, Instituto Superior Técnico, Lisboa, Portugal pdf

Abstract. One of the main goals of formalizing mathematics is to develop automation strategies/tactics that prove (partial) goals without requiring any input from the user. In this talk we show how to achieve this desideratum for the domain of real analysis in the proof assistant Coq, by defining ever more powerful tactics through two different strategies: the Auto with Hints mechanism and the use of Reflection.

The Fundamental Theorem of Calculus in Coq paper
24.Apr.2002 • TYPES 2002 Workshop, Berg en Dal, The Netherlands pdf

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 talk, 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.

Formalizing Mathematics in Coq
4.Jan.2002 • Theory of Computation Seminar, Instituto Superior Técnico, Lisboa, Portugal pdf

Computational Completeness of Combinatory Algebras
1.Jun.2001 • Theory of Computation Seminar, Instituto Superior Técnico, Lisboa, Portugal pdf

Abstract. Graduation thesis presentation.

Até Onde Podemos Ir?
24.Apr.2001 • Seminário Diagonal, Instituto Superior Técnico, Lisbon, Portugal pdf

Abstract. Ao longo do século XX os computadores passaram de inexistentes a indispensáveis, e hoje grande parte das tarefas do dia-a-dia é por eles realizada. Mas haverá um limite para o que podem fazer? Neste seminário veremos alguns resultados clássicos da Teoria da Computação, analisando algumas das suas consequências práticas. No final discutiremos o que os novos paradigmas de computação nos trazem de novo face aos tradicionais, e o que (não) devemos esperar deles.

Habilidades com Somatórios paper
24.Oct.2000 • Seminário Diagonal, Instituto Superior Técnico, Lisbon, Portugal pdf

Abstract. Alguns quebra-cabeças relativamente simples criam por vezes a necessidade de calcular somas pouco atraentes. Nesta apresentação 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.
No final, dar-se-ão pistas no sentido de resolver somatórios por métodos análogos aos utilizados na Teoria da Integração.