98 citations · 385 across the 33 of their papers we have counts for
7 papers · 1 filter
Now It Compiles! Certified Automatic Repair of Uncompilable Protocols
Luís Cruz-Filipe, Fabrizio Montesi
Choreographic programming is a paradigm where developers write the global specification (called choreography) of a communicating system, and then a correct-by-construction distribu…
A Formal Theory of Choreographic Programming
Luís Cruz-Filipe, Fabrizio Montesi, Marco Peressotti
Choreographic programming is a paradigm for writing coordination plans for distributed systems from a global point of view, from which correct-by-construction decentralised impleme…
Formalising a Turing-Complete Choreographic Language in Coq
Luís Cruz-Filipe, Fabrizio Montesi, Marco Peressotti
Theory of choreographic languages typically includes a number of complex results that are proved by structural induction. The high number of cases and the subtle details in some of…
Efficient Certified RAT Verification
Luís Cruz-Filipe, Marijn Heule, Warren Hunt +2
Clausal proofs have become a popular approach to validate the results of SAT solvers. However, validating clausal proofs in the most widely supported format (DRAT) is expensive eve…
Efficient Certified Resolution Proof Checking
Luís Cruz-Filipe, Joao Marques-Silva, Peter Schneider-Kamp
We present a novel propositional proof tracing format that eliminates complex processing, thus enabling efficient (formal) proof checking. The benefits of this format are demonstra…
Formalizing Size-Optimal Sorting Networks: Extracting a Certified Proof Checker
Luís Cruz-Filipe, Peter Schneider-Kamp
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…
Optimizing a Certified Proof Checker for a Large-Scale Computer-Generated Proof
Luís Cruz-Filipe, Peter Schneider-Kamp
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 compar…