Publications

To contribute to the web site, please open an issue, create a pull request or send a mail to the science communication coordinators.

STSM reports

• STSM reports

2024

• Learning Guided Automated Reasoning: A Brief Survey Lasse Blaauwbroek, David Cerna, Thibault Gauthier, Jan Jakubův, Cezary Kaliszyk, Martin Suda, Josef Urban, Arxiv, to appear. (Deliverable- D8)
• Generalisation through Negation and Predicate Invention, David M. Cerna and Andrew Cropper, AAAI-24, Feb. 22-25, to appear.
• Formal Specification and Verification of Architecturally-Defined Attestation Mechanisms in Arm CCA and Intel TDX, M. U. Sardar, T. Fossati, S. Frost, S. Xiong, IEEE Access, pp. 361-381, vol 12.

2023

• CICM’22 System Entries, P. Koepke, A. Lorenzen, B. Shminke, Intelligent Computer Mathematics. CICM 2022. Lecture Notes in Computer Science, vol 13467.
• Formalising Szemerédi’s Regularity Lemma and Roth’s Theorem on Arithmetic Progressions in Isabelle/HOL, Chelsea Edmonds, Angeliki Koutsoukou-Argyraki and Lawrence C. Paulson. Journal of Automated Reasoning, volume 67, Article number: 2 (2023).
• A Formalisation of the Balog-Szemerédi-Gowers Theorem in Isabelle/HOL, Angeliki Koutsoukou-Argyraki, Mantas Bakšys and Chelsea Edmonds. In Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP ’23), January 16–17, 2023, Boston, MA, USA. ACM, New York, NY, USA.
• Quantitative Global Memory, Sandra Alves, Delia Kesner, Miguel Ramos, WoLLIC’23
• A Rewriting Coherence Theorem with Applications in Homotopy Type Theory, Nicolai Kraus, Jakob von Raumer, MSCS
• A Semantics of 𝕂 into Dedukti, Amélie Ledein, Valentin Blot, Catherine Dubois, TYPES’22
• A modular construction of type theories, Frédéric Blanqui, Gilles Dowek, Emilie Grienenberger, Gabriel Hondet, François Thiré, LMCS
• Admissible Types-to-PERs Relativizations in Higher-Order Logic, Andrei Popescu, Dmitriy Traytel, POPL’23
• An Efficient Proof Checker and Elaborator for SMT Proofs in the Alethe Format, Bruno Andreotti, Hanna Lachnitt, Haniel Barbosa, TACAS’23
• An Interactive Interpretation Viewer for Typed First-order Logic, Jack McKeown, Geoff Sutcliffe, FLAIRS’23
• Anti-unification and Generalization: A Survey, David M. Cerna, Temur Kutsia, IJCAI’23
• Automated Completion of Statements and Proofs in Synthetic Geometry: an Approach based on Constraint Solving, Salwa Tabet Gonzalez, Predrag Janičić, Julien Narboux, ADG’23
• B-systems and C-systems are equivalent, Benedikt Ahrens, Jacopo Emmenegger, Paige R. North, Egbert Rijke, JSL
• Bases of pseudocompact Bishop spaces, Iosif Petrakis, Handbook of Constructive Mathematics
• Benchmarking Local Robustness of High-Accuracy Binary Neural Networks for Enhanced Traffic Sign Recognition, Andreea Postovan, Mădălina Eraşcu, FROM’23
• Capturing constrained constructor patterns in matching logic, Xiaohong Chen, Dorel Lucanu, Grigore Roşu, JLAMP
• Certified Compilation of Choreographies with hacc, Luís Cruz-Filipe, Lovro Lugovic, Fabrizio Montesi, FORTE’23
• Combining Higher-Order Logic with Set Theory Formalizations, Cezary Kaliszyk, Karol Pąk, JAR
• Competition on Software Verification and Witness Validation: SV-COMP 2023, Dirk Beyer, TACAS’23
• Composable partial multiparty session types for open systems, Claude Stolze, Marino Miculan, Pietro Di Gianantonio, SoSyM
• Currying Order and Restricted Algorithmic Beta-Conversion in Type Theory of Acyclic Recursion, Roussanka Loukanova, Logically Speaking. A Festschrift for Marie Duzi
• Eta-Reduction in Type-Theory of Acyclic Recursion, Roussanka Loukanova, ADCAIJ
• Evasiveness Through Binary Decision Diagrams, Jesús Aransay, Laureano Lambán, Julio Rubio, CICM’23
• Experiments on Infinite Model Finding in SMT Solving, Julian Parsert, Chad Brown, Mikolas Janota, Cezary Kaliszyk, LPAR’23
• Exploring Mathematical Conjecturing with Large Language Models, Moa Johansson, Nicholas Smallbone, NeSy’23
• Extending a High-Performance Prover to Higher-Order Logic, Petar Vukmirović, Jasmin Blanchette, Stephan Schulz, TACAS’23
• Flexible Automation of Quantified Multi-Modal Logics with Interaction, Melanie Taprogge, Alexander Steen, KI’23
• For the Metatheory of Type Theory, Internal Sconing Is Enough, Rafaël Bocquet, Ambrus Kaposi, Christian Sattler, FSCD’23
• Formula Normalizations in Verification, Simon Guilloud, Mario Bucev, Dragana Milovančević, Viktor Kunčak, CAV’23
• Hammering Floating-Point Arithmetic, Olle Torstensson, Tjark Weber, FroCoS’23
• Homotopy Type Theory as Internal Languages of Diagrams of ∞-Logoses, Taichi Uemura, FSCD’23
• How to frame innovation in mathematics, Bernhard Fisseni, Deniz Sarikaya, Bernhard Schröder, Synthese
• Keep me out of the loop: a more flexible choreographic projection, Luís Cruz-Filipe, Fabrizio Montesi, Robert R. Rasmussen, LPAR’23
• LISA: A Modern Proof System, Simon Guilloud, Sankalp Gambhir, Viktor Kunčak, ITP’23
• Learning Proof Transformations and Its Applications in Interactive Theorem Proving, Liao Zhang, Lasse Blaauwbroek, Cezary Kaliszyk, Josef Urban, FroCoS’23
• Lessons for Interactive Theorem Proving Researchers from a Survey of Coq Users, Ana de Almeida Borges, Annalí Casanueva Artís, Jean-Rémy Falleri, Emilio Jesús Gallego Arias, Érik Martin-Dorel, Karl Palmskog, Alexander Serebrenik, Théo Zimmermann, ITP’23
• Matching-Logic-Based Understanding of Polynomial Functors and their Initial/Final Models, Dorel Lucanu, FROM’23
• Measuring the Readability of Geometric Proofs—The Area Method Case, Pedro Quaresma, Pierluigi Graziani, JAR
• Mechanising Gödel–Löb Provability Logic in HOL Light, Marco Maggesi, Cosimo Perini Brogi, JAR
• MizAR 60 for Mizar 50, Jan Jakubův, Karel Chvalovský, Zarathustra Goertzel, Cezary Kaliszyk, Mirek Olšák, Bartosz Piotrowski, Stephan Schulz, Martin Suda, Josef Urban, ITP’23
• Multiple Query Satisfiability of Constrained Horn Clauses, Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti, PADL’23
• Now It Compiles! Certified Automatic Repair of Uncompilable Protocols, Luís Cruz-Filipe, Fabrizio Montesi, ITP’23
• On modified Halpern and Tikhonov-Mann iterations, Horațiu Cheval, Ulrich Kohlenbach, Laurentiu Leustean, J. Optim. Theor. Appl.
• Operationally-based program equivalence proofs using LCTRSs, Ştefan Ciobâcă, Dorel Lucanu, Andrei Sebastian Buruiană, JLAMP
• Parameterized Algebraic Protocols, Andreia Mordido, Janek Spaderna, Peter Thiemann, Vasco T. Vasconcelos, PLDI’23
• Program Synthesis in Saturation, Petra Hozzová, Laura Kovács, Chase Norman, Andrei Voronkov, CADE-29
• Proof-carrying parameters in certified symbolic execution, Andrei Arusoaie, Dorel Lucanu, LJIGPL
• Propositional Forms of Judgemental Interpretations, Tao Xue, Zhaohui Luo, Stergios Chatzikyriakidis, J. Log. Lang. Inf.
• QSMA: A New Algorithm for Quantified Satisfiability Modulo Theory and Assignment, Maria Paola Bonacina, Stéphane Graham-Lengrand, Christophe Vauthier, CADE’23
• Rates of asymptotic regularity for the alternating Halpern-Mann iteration, Laurentiu Leustean, Pedro Pinto, Optimization Letters
• Reconstruction of TLAPS Proofs Solved by VeriT in Lambdapi, Coltellacci Alessio, ABZ’23
• Representation, Verification, and Visualization of Tarskian Interpretations for Typed First-order Logic, Alexander Steen, Geoff Sutcliffe, Pascal Fontaine, Jack McKeown, LPAR’23
• Restricted Computations and Parameters in Type-Theory of Acyclic Recursion, Roussanka Loukanova, ADCAIJ
• Semantically-guided goal-sensitive reasoning: decision procedures and the Koala prover, Maria Paola Bonacina, Sarah Winkler, JAR
• Set-Theoretic and Type-Theoretic Ordinals Coincide, Tom de Jong, Nicolai Kraus, Fredrik Nordvall Forsberg, Chuangjie Xu, LICS’23
• Simple Type Theory: A Practical Logic for Expressing and Reasoning About Mathematical Ideas, William M. Farmer
• Solving Modal Logic Problems by Translation to Higher-order Logic, Alexander Steen, Geoff Sutcliffe, Tobias Scholl, Christoph Benzmüller, CLAR’23
• Solving the SPARQL query containment problem with SpeCS, Mirko Spasić, Milena Vujošević Janičić, J. Web Semant.
• Tableaux and sequent calculi for CTL and ECTL: Satisfiability test with certifying proofs and models, Alex Abuin, Alexander Bolotov, Montserrat Hermo, Paqui Lucio, JLAMP
• Tableaux for Realizability of Safety Specifications, Montserrat Hermo, Paqui Lucio, César Sánchez, FM’23
• Terms for Efficient Proof Checking and Parsing, Michael Färber, CPP’23
• Towards an Automatic Proof of the Bakery Algorithm, Aman Goel, Stephan Merz, Karem A. Sakallah, FORTE’23
• Translating proofs from an impredicative type system to a predicative one, Thiago Felicissimo, Frédéric Blanqui, Ashish Kumar Barnawal, CSL’23
• Two-level type theory and applications, Danil Annenkov, Paolo Capriotti, Nicolai Kraus, Christian Sattler, MSCS
• Type-theoretic approaches to ordinals, Nicolai Kraus, Fredrik Nordvall Forsberg, Chuangjie Xu, TCS
• Verification of mutable linear data structures and iterator-based algorithms in Dafny, Jorge Blázquez, Manuel Montenegro, Clara Segura, JLAMP
• Verification of the ROS NavFn planner using executable specification languages, Enrique Martín, Manuel Montenegro, Adrián Riesco, Juan Rodríguez-Hortalá, Rubén Rubio, JLAMP
• VizAR: Visualization of Automated Reasoning Proofs &endash; System Description, Jan Jakubův, Cezary Kaliszyk, CICM’23
• Who Finds the Short Proof? An Exploration of Variants of Boolos’ Curious Inference using Higher-order Automated Theorem Provers, Christoph Benzmüller, David Fuenmayor, Alexander Steen, Geoff Sutcliffe. LJIGPL
• Quantitative Global Memory, Sandra Alves, Delia Kesner, Miguel Ramos. WoLLIC 2023, Lecture Notes in Computer Science, vol 13923. Springer.

2022

• Irrationality and Transcendence Criteria for Infinite Series in Isabelle/HOL, Angeliki Koutsoukou-Argyraki, Wenda Li, and Lawrence C. Paulson, Experimental Mathematics, Special Issue on Interactive Theorem Proving in Mathematics Research, Volume 31, 2022 - Issue 2, pages 401-412.
• Formalising Ordinal Partition Relations Using Isabelle/HOL, Mirna Džamonja, Angeliki Koutsoukou-Argyraki, and Lawrence C. Paulson, Experimental Mathematics, Special Issue on Interactive Theorem Proving in Mathematics Research, Volume 31, 2022 - Issue 2, pages 383-400.
• Formal Entity Graphs as Complex Networks: Assessing Centrality Metrics of the Archive of Formal Proofs, Fabian Huch, In International Conference on Intelligent Computer Mathematics.
• Re-imagining the Isabelle Archive of Formal Proofs, MacKenzie, C., Huch, F., Vaughan, J., and Fleuriot, J. In International Conference on Intelligent Computer Mathematics.
• A Matching Logic Foundation for Alk, Alexandru-Ioan Lungu, Dorel Lucanu, ICTAC’22
• A Metatheoretic Analysis of Subtype Universes, Felix Bradley, Zhaohui Luo, TYPES’22
• Adequate and Computational Encodings in the Logical Framework Dedukti, Thiago Felicissimo, FSCD’22
• Algebras of complemented subsets, Iosif Petrakis, Daniel Wessel, CiE’22
• Algorithmic Dependent-Type Theory of Situated Information and Context Assessments, Roussanka Loukanova, DCAI’22
• An Extensible Logic Embedding Tool for Lightweight Non-Classical Reasoning, Alexander Steen, PAAR’22
• An Implementation of Set Theory with Pointed Graphs in Dedukti, Valentin Blot, Gilles Dowek, Thomas Traversié, LFMTP’22
• An extensible equality checking algorithm for dependent type theories, Andrej Bauer, Anja Petkovic Komel, LMCS
• Analysis and Transformation of Constrained Horn Clauses for Program Verification, Emanuele De Angelis, Fabio Fioravanti, John P. Gallagher, Manuel V. Hermenegildo, Alberto Pettorossi, Maurizio Proietti, TPLP
• Automated Reasoning in Non-classical Logics in the TPTP World, Alexander Steen, David Fuenmayor, Tobias Gleißner, Geoff Sutcliffe, Christoph Benzmüller, PAAR’22
• Automated Synthesis of Software Contracts with KINDSPEC, María Alpuente, Alicia Villanueva. Analysis, Verification and Transformation for Declarative Programming and Intelligent Systems. Lecture Notes in Computer Science, volume 13160, Springer.
• Bécassine à la chasse au Coq, Valentin Blot, Louise Dubois de Prisque, Chantal Keller, Pierre Vial, JFLA’22
• Bridging between LegalRuleML and TPTP for Automated Normative Reasoning, Alexander Steen, David Fuenmayor, RuleML+RR’22
• CDSAT for nondisjoint theories with shared predicates: arrays with abstract length, Maria Paola Bonacina, Stéphane Graham-Lengrand, Natarajan Shankar, SMT’22
• Closed subsets in Bishop topological groups, Iosif Petrakis, TCS
• Computability models over categories and presheaves, Iosif Petrakis, LFCS’22
• Conflict-driven satisfiability for theory combination: lemmas, modules, and proofs, Maria Paola Bonacina, Stéphane Graham-Lengrand, Natarajan Shankar, JAR
• Contract Strengthening through Constrained Horn Clause Verification, Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti, HCVS’22
• Contradiction Detection and Repair in Large Theories, Adam Pease, Stephan Schulz, FLAIRS’22
• Effective Kan Fibrations in Simplicial Sets, Benno van den Berg, Eric Faber
• Empirical Properties of Term Orderings for Superposition, Stephan Schulz, PAAR’22
• Encoding Type Universes Without Using Matching Modulo Associativity and Commutativity, Frédéric Blanqui, FSCD’22
• Evolution of Automated Deduction and Dynamic Constructions in Geometry, Pedro Quaresma, Mathematics Education in the Age of Artificial Intelligence, 2022
• Formalizing Alexander duality through BDDs, Jesús Aransay, Laureano Lambán, Julius Michaelis, Julio Rubio, ISAIM’22
• Four Geometry Problems to Introduce Automated Deduction in Secondary Schools, Pedro Quaresma, Vanda Santos, ThEdu’21
• Larry Wos – Visions of automated reasoning, Michael Beeson, Maria Paola Bonacina, Michael Kinyon, Geoff Sutcliffe, JAR
• Learning Higher-Order Logic Programs From Failures, Stanisław J. Purgał, David M. Cerna, Cezary Kaliszyk, IJCAI’22
• Lemmaless Induction in Trace Logic, Ahmed Bhayat, Pamina Georgiou, Clemens Eisenhofer, Laura Kovács, Giles Reger, CICM’22
• Mechanizing Matching Logic In Coq, Péter Bereczky, Xiaohong Chen, Dániel Horpácsi, Lucas Peña, Jan Tušil, FROM’22
• On Quantitative Algebraic Higher-Order Theories, Ugo Dal Lago, Furio Honsell, Marina Lenisa, Paolo Pistone, FSCD’22
• On SGGS and Horn clauses, Maria Paola Bonacina, Sarah Winkler, PAAR’22
• Proof-Carrying Parameters in Certified Symbolic Execution: The Case Study of Antiunification, Andrei Arusoaie, Dorel Lucanu, FROM’22
• Proof-relevance in Bishop-style constructive mathematics, Iosif Petrakis, MSCS
• Safe, Fast, Concurrent Proof Checking for the lambda-Pi Calculus Modulo Rewriting, Michael Färber, CPP’22
• Satisfiability of constrained Horn clauses on algebraic data types: A transformation-based approach, Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti, J. Log. Comput
• Set of support, demodulation, paramodulation: a historical perspective, Maria Paola Bonacina, JAR
• Sikkel: Multimode Simple Type Theory as an Agda Library, Joris Ceulemans, Andreas Nuyts, Dominique Devriese, MSFP’22
• Strict computability models over categories and presheaves, Iosif Petrakis, J. Log. Comput.
• The Logic Languages of the TPTP World, Geoff Sutcliffe, LJIGPL
• Theorem Proving for Maude Specifications Using Lean, Rubén Rubio, Adrián Riesco, ICFEM’22
• Verifying Catamorphism-Based Contracts using Constrained Horn Clauses, Emanuele De Angelis, Maurizio Proietti, Fabio Fioravanti, Alberto Pettorossi, TPLP
• Vers une traduction de K en Dedukti (Towards a translation of K in Dedukti), Amélie Ledein, Valentin Blot, Catherine Dubois, JFLA’22
• What Can Formal Systems Do For Mathematics? A Discussion Through The Lens Of Proof Assistants: Some Recent Advances, Angeliki Koutsoukou-Argyraki Q&A with Jeremy Avigad, Jasmin Blanchette, Frédéric Blanqui, Kevin Buzzard, Johan Commelin, Manuel Eberl, Timothy Gowers, Peter Koepke, Assia Mahboubi, Ursula Martin, Lawrence C. Paulson, Special Issue for the 60th Anniversary of the DVMLG (German Association for Mathematical Logic and for Basic Research in the Exact Sciences), Benedikt Löwe, Deniz Sarikaya (eds.), College Publications, 2022

Reports

• 2nd WG3 meeting, Timisoara, 8-9 February 2023, slides&videos report

• 1st WG3 meeting, Valencia, 10-11 February 2022 slides&videos report