Luís Cruz-Filipe

ACM Trans. Comput. Log., 2024

færdXel: An Expert System for Danish Traffic Law.

[BibT_eX]

[DOI]

Jonas Vistrup

CoRR, 2024

Minimizing Sorting Networks at the Sub-Comparator Level.

[BibT_eX]

[DOI]

Proceedings of the LPAR 2024: Proceedings of 25th Conference on Logic for Programming, 2024

Approximation Fixpoint Theory in Coq - With an Application to Logic Programming.

[BibT_eX]

[DOI]

Proceedings of the Logics and Type Systems in Theory and Practice, 2024

2023

A Formal Theory of Choreographic Programming.

[BibT_eX]

[DOI]

J. Autom. Reason., June, 2023

Keep me out of the loop: a more flexible choreographic projection.

[BibT_eX]

[DOI]

Robert R. Rasmussen

Proceedings of the LPAR 2023: Proceedings of 24th International Conference on Logic for Programming, 2023

Now It Compiles! Certified Automatic Repair of Uncompilable Protocols.

[BibT_eX]

[DOI]

Proceedings of the 14th International Conference on Interactive Theorem Proving, 2023

Certified Compilation of Choreographies with hacc.

[BibT_eX]

[DOI]

Lovro Lugovic

Proceedings of the Formal Techniques for Distributed Objects, Components, and Systems, 2023

Modular Compilation for Higher-Order Functional Choreographies.

[BibT_eX]

[DOI]

Proceedings of the 37th European Conference on Object-Oriented Programming, 2023

Reasoning About Choreographic Programs.

[BibT_eX]

[DOI]

Proceedings of the Coordination Models and Languages, 2023

2022

Implementing Choreography Extraction.

[BibT_eX]

[DOI]

CoRR, 2022

Modular Choreographies: Bridging Alice and Bob Notation to Java.

[BibT_eX]

[DOI]

Proceedings of the Joint Post-proceedings of the Third and Fourth International Conference on Microservices, 2022

From Infinity to Choreographies - Extraction for Unbounded Systems.

[BibT_eX]

[DOI]

Bjørn Angel Kjær

Proceedings of the Logic-Based Program Synthesis and Transformation, 2022

Reconciling Communication Delays and Negation.

[BibT_eX]

[DOI]

Proceedings of the Theoretical Aspects of Computing - ICTAC 2022, 2022

Functional Choreographic Programming.

[BibT_eX]

[DOI]

Proceedings of the Theoretical Aspects of Computing - ICTAC 2022, 2022

Can You Answer While You Wait?

[BibT_eX]

[DOI]

Proceedings of the Foundations of Information and Knowledge Systems, 2022

2021

Stratification in Approximation Fixpoint Theory and Its Application to Active Integrity Constraints.

[BibT_eX]

[DOI]

ACM Trans. Comput. Log., 2021

Choreographies as Functions.

[BibT_eX]

[DOI]

CoRR, 2021

Formalising a Turing-Complete Choreographic Language in Coq.

[BibT_eX]

[DOI]

Proceedings of the 12th International Conference on Interactive Theorem Proving, 2021

Certifying Choreography Compilation.

[BibT_eX]

[DOI]

Proceedings of the Theoretical Aspects of Computing - ICTAC 2021, 2021

2020

A core model for choreographic programming.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 2020

2019

Sorting networks: To the end and back again.

[BibT_eX]

[DOI]

J. Comput. Syst. Sci., 2019

Formally Verifying the Solution to the Boolean Pythagorean Triples Problem.

[BibT_eX]

[DOI]

João Marques-Silva

J. Autom. Reason., 2019

Implementing choreography extraction.

[BibT_eX]

[DOI]

Larisa Safina

CoRR, 2019

2018

Machine-Assisted Proofs (ICM 2018 Panel).

[BibT_eX]

[DOI]

CoRR, 2018

Connectors meet Choreographies.

[BibT_eX]

[DOI]

CoRR, 2018

Active integrity constraints for general-purpose knowledge bases.

[BibT_eX]

[DOI]

Ann. Math. Artif. Intell., 2018

Fixpoint semantics for active integrity constraints.

[BibT_eX]

[DOI]

Artif. Intell., 2018

Communications in choreographies, revisited.

[BibT_eX]

[DOI]

Proceedings of the 33rd Annual ACM Symposium on Applied Computing, 2018

Multiparty Classical Choreographies.

[BibT_eX]

[DOI]

Proceedings of the Logic-Based Program Synthesis and Transformation, 2018

Complete and Efficient DRAT Proof Checking.

[BibT_eX]

[DOI]

Adrian Rebola-Pardo

Proceedings of the 2018 Formal Methods in Computer Aided Design, 2018

2017

From description-logic programs to multi-context systems.

[BibT_eX]

[DOI]

J. Log. Algebraic Methods Program., 2017

Optimal-depth sorting networks.

[BibT_eX]

[DOI]

J. Comput. Syst. Sci., 2017

Formally Proving Size Optimality of Sorting Networks.

[BibT_eX]

[DOI]

Kim S. Larsen

J. Autom. Reason., 2017

Optimizing sorting algorithms by using sorting networks.

[BibT_eX]

[DOI]

Formal Aspects Comput., 2017

On Asynchrony and Choreographies.

[BibT_eX]

[DOI]

Proceedings of the Proceedings 10th Interaction and Concurrency Experience, 2017

That's Enough: Asynchrony with Standard Choreography Primitives.

[BibT_eX]

[DOI]

CoRR, 2017

Efficient Certified Resolution Proof Checking.

[BibT_eX]

[DOI]

João Marques-Silva

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2017

Encoding asynchrony in choreographies.

[BibT_eX]

[DOI]

Proceedings of the Symposium on Applied Computing, 2017

Formally Proving the Boolean Pythagorean Triples Conjecture.

[BibT_eX]

[DOI]

Proceedings of the LPAR-21, 2017

How to Get More Out of Your Oracles.

[BibT_eX]

[DOI]

Kim S. Larsen

Proceedings of the Interactive Theorem Proving - 8th International Conference, 2017

Semantics for Active Integrity Constraints Using Approximation Fixpoint Theory.

[BibT_eX]

[DOI]

Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence, 2017

The Paths to Choreography Extraction.

[BibT_eX]

[DOI]

Kim S. Larsen

Proceedings of the Foundations of Software Science and Computation Structures, 2017

Procedural Choreographic Programming.

[BibT_eX]

[DOI]

Proceedings of the Formal Techniques for Distributed Objects, Components, and Systems, 2017

Efficient Certified RAT Verification.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction - CADE 26, 2017

2016

Sorting nine inputs requires twenty-five comparisons.

[BibT_eX]

[DOI]

J. Comput. Syst. Sci., 2016

Choreographies, Divided and Conquered.

[BibT_eX]

[DOI]

CoRR, 2016

Grounded Fixpoints and Active Integrity Constraints.

[BibT_eX]

[DOI]

Proceedings of the Technical Communications of the 32nd International Conference on Logic Programming, 2016

Choreographies in Practice.

[BibT_eX]

[DOI]

Proceedings of the Formal Techniques for Distributed Objects, Components, and Systems, 2016

Integrity Constraints for General-Purpose Knowledge Bases.

[BibT_eX]

[DOI]

Proceedings of the Foundations of Information and Knowledge Systems, 2016

Active Integrity Constraints for Multi-context Systems.

[BibT_eX]

[DOI]

Proceedings of the Knowledge Engineering and Knowledge Management, 2016

2015

The Finitistic Consistency of Heck's Predicative Fregean System.

[BibT_eX]

[DOI]

Fernando Ferreira

Notre Dame J. Formal Log., 2015

Choreographies, Computationally.

[BibT_eX]

[DOI]

CoRR, 2015

repAIrC: A Tool for Ensuring Data Consistency by Means of Active Integrity Constraints.

[BibT_eX]

[DOI]

CoRR, 2015

When Six Gates are Not Enough.

[BibT_eX]

[DOI]

CoRR, 2015

Optimizing a Certified Proof Checker for a Large-Scale Computer-Generated Proof.

[BibT_eX]

[DOI]

Proceedings of the Intelligent Computer Mathematics - International Conference, 2015

Applying Sorting Networks to Synthesize Optimized Sorting Libraries.

[BibT_eX]

[DOI]

Proceedings of the Logic-Based Program Synthesis and Transformation, 2015

Sorting Networks: The End Game.

[BibT_eX]

[DOI]

Michael Codish

Proceedings of the Language and Automata Theory and Applications, 2015

Formalizing Size-Optimal Sorting Networks: Extracting a Certified Proof Checker.

[BibT_eX]

[DOI]

Vasco Thudichum Vasconcelos

Proceedings of the Interactive Theorem Proving - 6th International Conference, 2015

Active Integrity Constraints: From Theory to Implementation.

[BibT_eX]

[DOI]

Proceedings of the Knowledge Discovery, Knowledge Engineering and Knowledge Management, 2015

repAIrC: A Tool for Ensuring Data Consistency.

[BibT_eX]

[DOI]

Proceedings of the KMIS 2015, 2015

2014

The stream-based service-centred calculus: a foundation for service-oriented programming.

[BibT_eX]

[DOI]

Formal Aspects Comput., 2014

The Quest for Optimal Sorting Networks: Efficient Generation of Two-Layer Prefixes.

[BibT_eX]

[DOI]

Michael Codish

Proceedings of the 16th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, 2014

Twenty-Five Comparators Is Optimal When Sorting Nine Inputs (and Twenty-Nine for Ten).

[BibT_eX]

[DOI]

Proceedings of the 26th IEEE International Conference on Tools with Artificial Intelligence, 2014

Optimizing Computation of Repairs from Active Integrity Constraints.

[BibT_eX]

[DOI]

Proceedings of the Foundations of Information and Knowledge Systems, 2014

Information Flow within Relational Multi-context Systems.

[BibT_eX]

[DOI]

Proceedings of the Knowledge Engineering and Knowledge Management, 2014

2013

Computing Repairs from Active Integrity Constraints.

[BibT_eX]

[DOI]

Proceedings of the Seventh International Symposium on Theoretical Aspects of Software Engineering, 2013

Description Logics, Rules and Multi-context Systems.

[BibT_eX]

[DOI]

Rita Henriques

Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2013

Patterns for Interfacing between Logic Programs and Multiple Ontologies.

[BibT_eX]

[DOI]

Proceedings of the KEOD 2013, 2013

Design Patterns for Description-Logic Programs.

[BibT_eX]

[DOI]

Proceedings of the Knowledge Discovery, Knowledge Engineering and Knowledge Management, 2013

2008

Complete Axiomatization of Discrete-Measure Almost-Everywhere Quantification.

[BibT_eX]

[DOI]

J. Log. Comput., 2008

Heterogeneous Fibring of Deductive Systems Via Abstract Proof Systems.

[BibT_eX]

[DOI]

Vasco Thudichum Vasconcelos

Amílcar Sernadas

Cristina Sernadas

Log. J. IGPL, 2008

Behavioural Theory at Work: Program Transformations in a Service-Centred Calculus.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods for Open Object-Based Distributed Systems, 2008

2007

Reasoning about probabilistic sequential programs.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 2007

2005

A Large-Scale Experiment in Executing Extracted Programs.

[BibT_eX]

[DOI]

Pierre Letouzey

Proceedings of the 12th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning, 2005

2004

Hierarchical Reflection.

[BibT_eX]

[DOI]

Freek Wiedijk

Proceedings of the Theorem Proving in Higher Order Logics, 17th International Conference, 2004

C-CoRN, the Constructive Coq Repository at Nijmegen.

[BibT_eX]

[DOI]

Herman Geuvers

Freek Wiedijk

Proceedings of the Mathematical Knowledge Management, Third International Conference, 2004

2003

Program Extraction from Large Proof Developments.

[BibT_eX]

[DOI]

Bas Spitters

Proceedings of the Theorem Proving in Higher Order Logics, 16th International Conference, 2003

2002

A Constructive Formalization of the Fundamental Theorem of Calculus.

[BibT_eX]

[DOI]