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

2025

• 2-Functoriality of Initial Semantics, and Applications, Benedikt Ahrens, Ambroise Lafont, Thomas Lamiaux, ICFP’25
• A New Approach for Showing Termination of Parameterized Transition Systems, Roland Herrmann, Philipp Rümmer, CIAA’25
• A Predicative Approach to the Constructive Integration Theory of Locally Compact Metric Spaces, Fabian Lukas Grubmüller, Iosif Petrakis. J. Log. Anal.
• A quantitative approach to global state composition, Sandra Alves, Delia Kesner, Miguel Ramos, MSCS
• ADG Lib Initiative, Pedro Quaresma, Predrag Janičić, Julien Narboux, Zoltán Kovács, Anna Petiurenko, Filip Marić and Nuno Baeta, extended abstract at ADG’25
• An iterative constructive Hilbert basis theorem, Peter Schuster, Ihsen Yengui, *J. Algebra
• Animating MRBNFs: Truly Modular Binding-Aware Datatypes in Isabelle/HOL, Jan van Brügge, Andrei Popescu, Dmitriy Traytel, ITP’25
• Arithmetizing Shape Analysis, Sebastian Wolff, Ekanshdeep Gupta, Zafer Esen, Hossein Hojjat, Philipp Rümmer, Thomas Wies, CAV’25
• Barendregt Convenes with Knaster and Tarski: Strong Rule Induction for Syntax with Bindings, Jan van Brügge, James McKinna, Andrei Popescu, Dmitriy Traytel, POPL’25
• BiSikkel: A Multimode Logical Framework in Agda., Joris Ceulemans, Andreas Nuyts, Dominique Devriese, POPL’25
• Boolean Rigs, Daniel Misselbeck-Wessel, Iosif Petrakis, Algebra Universalis
• Case Study: Verified Vampire Proofs in the LambdaPi-calculus Modulo, Anja Petkovic Komel, Michael Rawson, Martin Suda. arXiv
• Checking Linear Integer Arithmetic Proofs in LambdaPi, Alessio Coltellacci, Stephan Merz, FroCoS’25
• Comodule Representations of Second-Order Functionals, Danel Ahman, Andrej Bauer. JLAMP
• Complementable Normal Form of Parametrized Automata, Franziska Alber, Philipp Rümmer, CIAA’25
• Conservation as translation, Giulio Fellin, Peter Schuster, Rev. Symb. Log.
• Continuous and algebraic domains in univalent foundations, Tom de Jong, Martín Hötzel Escardó, Journal of Pure and Applied Algebra
• Coverage Semantics for Dependent Pattern Matching, Joseph Eremondi and Ohad Kammar, ESOP’25
• Epimorphisms and Acyclic Types in Univalent Foundations, Ulrik Buchholtz, Tom de Jong, Egbert Rijke, Journal of Symbolic Logic
• Equational Reasoning Modulo Commutativity in Languages with Binders, Ali K. Caires-Santos, Maribel Fernández, Daniele Nantes-Sobrinho, CADE’25
• Formalising Inductive and Coinductive Containers, Stefania Damato, Thorsten Altenkirch, Axel Ljungström, ITP’25
• Formalizing Equivalences Without Tears, Tom de Jong, TYPES’24 post-proceedings
• Frex: dependently-typed algebraic simplification, Guillaume Allais, Edwin Brady, Nathan Corbyn, Ohad Kammar, and Jeremy Yallop, ICFP’25
• Ground Truth: Checking Vampire Proofs via Satisfiability Modulo Theories, Michael Rawson, Andrei Voronkov, Johannes Schoisswohl, Anja Petkovic Komel. CADE 2025
• Improving the SMT Proof Reconstruction Pipeline in Isabelle/HOL, Hanna Lachnitt, Mathias Fleury, Haniel Barbosa, Andrew Reynolds, Jibiana Jakpor, Bruno Andreotti, Clark Barrett, Hans-Joerg Schurr, and Cesare Tinelli, ITP’25
• lean-smt: An SMT Tactic for Discharging Proof Goals in Lean., Abdalrhman Mohamed, Tomaz Mascarenhas, Muhammad Harun Ali Khan, Haniel Barbosa, Andrew Reynolds, Yicheng Qian, Cesare Tinelli, Clark W. Barrett. CAV 2025
• Modelling Recursion and Probabilistic Choice in Guarded Type Theory, Philipp Stassen, Rasmus Ejlers Møgelberg, Maaike Zwart, Alejandro Aguirre, Lars Birkedal, POPL’25
• Modular Sequent Calculi for interpretability Logics, Cosimo Perini Brogi, Sara Negri, Nicola Olivetti, Rev. Symb. Log.
• Multimode Type Theory as a Library in Type Theory, Joris Ceulemans, Dominique Devriese (sup.), Andreas Nuyts (co-sup.), PhD dissertation @ KU Leuven
• Nominal Matching Logic with Fixpoints, Mircea Sebe, Maribel Fernández, James Cheney, CPP’25
• On the Limitations of ROBDDs in Deciding the Evasiveness of Boolean Functions, Jesús Aransay, Laureano Lambán, Julio Rubio, Discret. math. lett.
• Ordinal Exponentiation in Homotopy Type Theory, Tom de Jong, Nicolai Kraus, Fredrik Nordvall Forsberg, Chuangjie Xu, LICS’25
• Practically Feasible Proof Logging for Pseudo-Boolean Optimization, Wietze Koops, Daniel Le Berre, Magnus O. Myreen, Jakob Nordström, Andy Oertel, Yong Kiam Tan, Marc Vinyals, CP’25
• Projective Delineability for Single Cell Construction, Jasper Nalbach, Lucas Michel, Erika Ábrahám, Christopher W. Brown, James H. Davenport, Matthew England, Pierre Mathonet, Naïm Zénaïdi. arXiv
• Proof Search in Classical Propositional Logic with Partial Proof Terms, José Espírito Santo, Ana Catarina Sousa, WoLLIC’25
• Proof Verification with GDV and LambdaPi - It’s a Matter of Trust, Geoff Sutcliffe, Frédéric Blanqui, Guillaume Burel, FLAIRS’25
• Proving Correctness of the Query Containment Solver SpeCS using SPARQL Set Semantics, Mirko Spasić, Milena Vujošević Janičić. J. Web Semant.
• Pseudo-Boolean Proof Logging for Optimal Classical Planning, Simon Dold, Malte Helmert, Jakob Nordström, Gabriele Röger, Tanja Schindler, ICAPS’25
• Safely Encoding B Proof Obligations in SMT-LIB, Vincent Trélat, ABZ 2025
• Scalable Knowledge Refactoring using Constrained Optimisation, Minghao Liu, David M. Cerna, Filipe Gouveia, Andrew Cropper, AAAI’25
• Separate but Together: Integrating Remote Attestation into TLS, Carsten Weinhold, Muhammad Usama Sardar, Ionut Mihalcea, Yogesh Deshpande, Hannes Tschofenig, Yaron Sheffer, Thomas Fossati, Michael Roitzsch, USENIX ATC’25
• Shared Terms and Cached Rewriting, Stephan Schulz, IWIL’24
• Solving Quantified Modal Logic Problems by Translation to Classical Logics, Alexander Steen, Geoff Sutcliffe, Christoph Benzmüller. Journal of Logic and Computation
• Strong negation in the theory of computable functionals TCF, Nils Köpp, Iosif Petrakis, LMCS
• Text Homology, Jesús Aransay, Laureano Lambán, Julio Rubio, J. Quant. Linguistics
• The CDSAT method for satisfiability modulo theories and assignments: an exposition, Maria Paola Bonacina, CiE’25
• The Cost of Skeletal Call-by-Need, Smoothly, Beniamino Accattoli, Francesco Magliocca, Loïc Peyrot, Claudio Sacerdoti Coen, FSCD’25
• The Grothendieck Computability Model, Luis Gambarte, Iosif Petrakis, TCS
• The QSMA algorithm for quantifiers in SMT., Maria Paola Bonacina, Stéphane Graham-Lengrand, and Christophe Vauthier, JAR
• Type Theory in Type Theory using a Strictified Syntax, Ambrus Kaposi, Loïc Pujet, ICFP’25
• What’s Decidable About Arrays With Sums?, Roland Herrmann, Philipp Rümmer, CADE’25

2024

• A Constraint Solving Approach to Parikh Images of Regular Languages, Amanda Stjerna, Philipp Rümmer, OOPSLA’24
• A Formalization of the General Theory of Quaternions, Thaynara Arielly de Lima, André Luiz Galdino, Bruno Berto de Oliveira Ribeiro, Mauricio Ayala-Rincón, ITP’24
• A General Constructive Form of Higman’s Lemma, Stefano Berardi, Gabriele Buriola, Peter Schuster, CSL’24
• A Matroid-Based Automatic Prover and Coq Proof Generator for Projective Incidence Geometry, David Braun, Nicolas Magaud, Pascal Schreck, JAR
• A Modular Formalization of Superposition in Isabelle/HOL, Martin Desharnais, Balázs Tóth, Uwe Waldmann, Jasmin Blanchette, Sophie Tourret, ITP’24
• A Proof-Theoretic Approach to Formal Epistemology, Sara Negri, Edi Pavlović. Saul Kripke on Modal Logic
• A Sound and Complete Algorithm to Identify Independent Variables in a Reactive System Specification, Josu Oca, Montserrat Hermo, Alexander Bolotov, DATE’24
• A Sound and Complete Substitution Algorithm for Multimode Type Theory, Joris Ceulemans, Andreas Nuyts, Dominique Devriese, TYPES’23 post-proceedings
• A Tree Rewriting System for the Reflection Calculus, Sofía Santiago-Fernández, Joost J. Joosten, David Fernández-Duque, AiML’24
• Alk: A Formal-Methods-based Educational Platform for Enhancing Algorithmic Thinking, Alexandru{-}Ioan Lungu, Vlad Teodorescu, Andrei Zaborila, Oana Andrei, Dorel Lucanu. Sci. Ann. Comput. Sci.
• Analysing Collective Adaptive Systems by Proving Theorems, Cosimo Perini Brogi, Marco Maggesi, ISoLA’24
• Automatic Verification of SMT Rewrites in Isabelle/HOL, Hanna Lachnitt, Mathias Fleury, Leni Aniva, Andrew Reynolds, Haniel Barbosa, Andres Nötzli, Clark W. Barrett, Cesare Tinelli, TACAS’24
• Automating Boundary Filling in Cubical Agda, Maximilian Doré, Evan Cavallo, Anders Mörtberg, FSCD’24
• Certified First-Order AC-Unification and Applications, Mauricio Ayala-Rincón, Maribel Fernández, Gabriel Ferreira Silva, Temur Kutsia, Daniele Nantes-Sobrinho, JAR
• Certified MaxSAT Preprocessing, Hannes Ihalainen, Andy Oertel, Yong Kiam Tan, Jeremias Berg, Matti Järvisalo, Magnus O. Myreen, Jakob Nordström, IJCAR’24
• Certifying Incremental SAT Solving, Katalin Fazekas, Florian Pollitt, Mathias Fleury, Armin Biere, LPAR’24
• Certifying MIP-based Presolve Reductions for 0-1 Integer Linear Programs, Alexander Hoen, Andy Oertel, Ambros Gleixner, Jakob Nordström, CPAIOR’24
• Certifying Without Loss of Generality Reasoning in Solution-Improving Maximum Satisfiability, Jeremias Berg, Bart Bogaerts, Jakob Nordström, Andy Oertel, Tobias Paxian, Dieter Vandesande, CP’24
• Clausal Congruence Closure, Armin Biere, Katalin Fazekas, Mathias Fleury, Nils Froleyks, SAT’24
• Clausal Equivalence Sweeping, Armin Biere, Katalin Fazekas, Mathias Fleury, Nils Froleyks, FMCAD’24
• Comodule Representations of Second-Order Functionals, Danel Ahman, Andrej Bauer, arXiv
• Complemented Subsets and Boolean-valued, Partial Functions, Daniel Misselbeck-Wessel, Iosif Petrakis, Comput.
• Conway Normal Form: Bridging Approaches for Comprehensive Formalization of Surreal Numbers, Karol Pąk, Cezary Kaliszyk, ITP’24
• Deductive Verification of Sparse Sets in Why3, Catherine Dubois, VSTTE’24
• Differentiable Inductive Logic Programming in High-Dimensional Space, Stanisław J. Purgał, David M. Cerna, Cezary Kaliszyk, IJCLR’24
• End-to-End Verification for Subgraph Solving, Stephan Gocht, Ciaran McCreesh, Magnus O. Myreen, Jakob Nordström, Andy Oertel, Yong Kiam Tan, AAAI’24
• Equational Anti-unification over Absorption Theories, Mauricio Ayala-Rincón, David M. Cerna, Andres Felipe Gonzalez Barragan, Temur Kutsia, IJCAR’24
• 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
• G3-style Sequent Calculi for Gurevich Logic and Its Neighbors, Norihiro Kamide, Sara Negri, Studia Logica
• Generalisation through Negation and Predicate Invention, David M. Cerna, Andrew Cropper, AAAI’24
• HOL Light to Isabelle/HOL Translation, Rebooted, Ghilain Bergeron, Stéphane Glondu, Sophie Tourret, Isabelle’24
• IMELL Cut Elimination with Linear Overhead, Beniamino Accattoli, Claudio Sacerdoti Coen, FSCD’24
• Internal and Observational Parametricity for Cubical Agda, Antoine Van Muylder, Andreas Nuyts, Dominique Devriese, POPL’24
• Interpolation and Quantifiers in Ortholattices, Simon Guilloud, Sankalp Gambhir, Viktor Kunčak, VMCAI’24
• Invited Talk: The Hows and Whys of Higher-Order SMT, Sophie Tourret, SMT’24
• Isabelle-Verified Correctness of Datalog Programs for Program Analysis, Anders Schlichtkrull, René Rydhof Hansen, Flemming Nielson, SAC’24
• IsaRare: Automatic Verification of SMT Rewrites in Isabelle/HOL., Hanna Lachnitt, Mathias Fleury, Leni Aniva, Andrew Reynolds, Haniel Barbosa, Andres Nötzli, Clark W. Barrett, Cesare Tinelli, TACAS’24
• Isomorphic Transfer Infrastructure for Nested Types in Isabelle/HOL (Work in Progress), Gergely Buday, Andrei Popescu. PhD@IFM’24
• Kuroda’s Translation for the λΠ-Calculus Modulo Theory and Dedukti, Thomas Traversié, LFMTP’24
• Lazy and Eager Patterns in High-Performance Automated Theorem Proving, Stephan Schulz, Vampire’24
• Lazy Reimplication in Chronological Backtracking, Robin Coutelier, Mathias Fleury and Laura Kovács, SAT’24
• Learn to Unlearn, Bernhard Gstrein and Florian Pollitt and André Schidler and Mathias Fleury and Armin Biere, SAT’24
• Learning Guided Automated Reasoning: A Brief Survey, Lasse Blaauwbroek, David M. Cerna, Thibault Gauthier, Jan Jakubův, Cezary Kaliszyk, Martin Suda, Josef Urban. Logics and Type Systems in Theory and Practice 2024
• Learning Rules Explaining Interactive Theorem Proving Tactic Prediction, Liao Zhang, David M. Cerna, Cezary Kaliszyk, IJCLR’24
• Learning Structure-Aware Representations of Dependent Types, Konstantinos Kogkalidis, Orestis Melkonian, Jean-Philippe Bernardy, NeurIPS’24
• Lemma Discovery and Strategies for Automated Induction, Sólrún Halla Einarsdóttir, Márton Hajdú, Moa Johansson, Nicholas Smallbone, Martin Suda, IJCAR’24
• Maude2Lean: Theorem proving for Maude specifications using Lean, Rubén Rubio, Adrián Riesco, JLAMP
• Mechanized HOL Reasoning in Set Theory, Simon Guilloud, Sankalp Gambhir, Andrea Gilot, Viktor Kunčak, ITP’24
• On Projective Delineability, Lucas Michel, Jasper Nalbach, Pierre Mathonet, Naïm Zénaïdi, Christopher W. Brown, Erika Ábrahám, James H. Davenport, Matthew England, SYNASC’24
• OnlineProver: Experience with a Visualisation Tool for Teaching Formal Proofs, Ján Perhác, Samuel Novotný, Sergej Chodarev, Joachim Tilsted Kristensen, Lars Tveito, Oleks Shturmov, Michael Kirkedal Thomsen. ThEdu@CADE’24
• Orthologic with Axioms, Simon Guilloud, Viktor Kunčak, POPL’24
• Partial Proof Terms in the Study of Idealized Proof Search, José Espírito Santo, Ana Catarina Sousa, CICM’24
• Pre-measure Spaces and Pre-integration Spaces in Predicative Bishop-Cheng Measure Theory, Iosif Petrakis, Max Zeuner, LMCS
• Proof exploration using dynamic geometry systems with integrated automated deduction capabilities, Pedro Quaresma, Vanda Santos, Joana Teles, IJMEST
• Proof Logging for the Circuit Constraint, Matthew McIlree, Ciaran McCreesh, Jakob Nordström, CPAIOR’24
• Proof-carrying Parameters in Certified Symbolic Execution, Andrei Arusoaie, Dorel Lucanu, LJIGPL
• Proofs for Free in the λΠ-Calculus Modulo Theory, Thomas Traversié, LFMTP’24
• Pseudo-Boolean Reasoning About States and Transitions to Certify Dynamic Programming and Decision Diagram Algorithms, Emir Demirović, Ciaran McCreesh, Matthew McIlree, Jakob Nordström, Andy Oertel, Konstantin Sidorov, CP’24
• Reasoning in Transformers - Mitigating Spurious Correlations and Reasoning Shortcuts, Daniel Enström, Viktor Kjellberg, Moa Johansson, NeSy’24
• Reifying dynamical algebra: Maximal ideals in countable rings, constructively, Ingo Blechschmidt, Peter Schuster, Computability
• Rigorous Analysis of Idealised Pathfinding Ants in Higher-Order Logic, Marco Maggesi, Cosimo Perini Brogi, ISoLA’24
• Satisfiability Modulo Theories: A Beginner’s Tutorial, Clark W. Barrett, Cesare Tinelli, Haniel Barbosa, Aina Niemetz, Mathias Preiner, Andrew Reynolds, Yoni Zohar, FM’24
• SC-TPTP: An Extension of the TPTP Derivation Format for Sequent-Based Calculus, Julie Cailler, Simon Guilloud, PAAR’24
• Second-Order Generalised Algebraic Theories: Signatures and First-Order Semantics, Ambrus Kaposi, Szumi Xie, FSCD’24
• Sets Completely Separated by Functions in Bishop Set Theory, Iosif Petrakis. Notre Dame J. Formal Logic
• Sharing proofs with predicative theories through universe-polymorphic elaboration, Thiago Felicissimo, Frédéric Blanqui, LMCS
• Shoggoth: A Formal Foundation for Strategic Rewriting, Xueying Qin, Liam O’Connor, Rob van Glabbeek, Peter Höfner, Ohad Kammar, and Michel Steuwer, POPL’24
• Some Decidability Issues Concerning Cⁿ Real Functions, Gabriele Buriola, Domenico Cantone, Giuseppe Cincotti, Eugenio G. Omodeo, Giuseppe T. Spartà, CILC’24
• Specification Languages for Computational Laws Versus Basic Legal Principles, Petia Guintchev, Joost J. Joosten, Sofía Santiago-Fernández, Eric Sancho Adamson, Aleix Solé Sánchez, Marta Soria Heredia. arXiv
• Specify What? Enhancing Neural Specification Synthesis by Symbolic Methods, George Granberry, Wolfgang Ahrendt, Moa Johansson, IFM’24
• Strictly Positive Fragments of the Provability Logic of Heyting Arithmetic, Ana de Almeida Borges, Joost J. Joosten . Studia Logica
• The Grothendieck Computability Model, Luis Gambarte, Iosif Petrakis, ICTCS’24
• The MoXI Model Exchange Tool Suite, Chris Johannsen, Karthik Nukala, Rohit Dureja, Ahmed Irfan, Natarajan Shankar, Cesare Tinelli, Moshe Y. Vardi, Kristin Yvonne Rozier, CAV’24
• The New TPTP Format for Interpretations, Geoff Sutcliffe, Alexander Steen, Pascal Fontaine
• Towards a Readability Criterion for Humans and Machines, Pedro Quaresma, Pierluigi Graziani, SEFM’24
• Towards Multilingual Autoformalization and Informalization of Mathematics, Aarne Ranta, SLTC’24
• Towards Producing Shorter Congruence Closure Proofs in a State-of-the-art SMT Solver (Extended Abstract), Bruno Andreotti, Haniel Barbosa, Oliver Flatt, PAAR’24
• Towards the Exact Complexity of Realizability for Safety LTL, Noel Arteche, Montserrat Hermo, JLAMP
• Towards Validation of TLS 1.3 Formal Model and Vulnerabilities in Intel’s RA-TLS Protocol, Muhammad Usama Sardar, Arto Niemi, Hannes Tschofenig, Thomas Fossati. IEEE Access
• Translating HOL-Light proofs to Coq, Frédéric Blanqui, LPAR’24
• Transpension: The Right Adjoint to the Pi-type, Andreas Nuyts, Dominique Devriese, LMCS
• Type-Theory of Algorithms with Chain-Free Memory, Roussanka Loukanova, DCAI’24
• Universal algebra in UniMath, Gianluca Amato, Matteo Calosci, Marco Maggesi, Cosimo Perini Brogi, MSCS
• UTC Time, Formally Verified, Ana de Almeida Borges, Mireia González Bedmar, Juan Conejero Rodríguez, Eduardo Hermo Reyes, Joaquim Casals Buñuel, Joost Joosten. CPP24
• What Monads Can and Cannot Do with a Bit of Extra Time, Rasmus Ejlers Møgelberg, Maaike Zwart, CSL’24
• Who finds the short proof?, Christoph Benzmüller, David Fuenmayor, Alexander Steen, Geoff Sutcliffe, LJIGPL

2023

• A Constructive Picture of Noetherian Conditions and Well Quasi-orders, Gabriele Buriola, Peter Schuster, Ingo Blechschmidt, CiE’23
• A Formalisation of the Balog-Szemerédi-Gowers Theorem in Isabelle/HOL, Angeliki Koutsoukou-Argyraki, Mantas Bakšys and Chelsea Edmonds, CPP’23
• A modular construction of type theories, Frédéric Blanqui, Gilles Dowek, Emilie Grienenberger, Gabriel Hondet, François Thiré, LMCS
• A More Pragmatic {CDCL} for IsaSAT and Targetting {LLVM} (Short Paper), Mathias Fleury, Peter Lammich, CADE’29 (2023)
• 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 post-proceedings
• Admissible Types-to-PERs Relativizations in Higher-Order Logic, Andrei Popescu, Dmitriy Traytel, POPL’23
• An Active Learning Approach to Synthesizing Program Contracts, Sandip Ghosal, Bengt Jonsson, Philipp Rümmer, SEFM’23
• An Efficient Proof Checker and Elaborator for SMT Proofs in the Alethe Format, Bruno Andreotti, Hanna Lachnitt, Haniel Barbosa, TACAS’23
• An Encoding of Abstract Dialectical Frameworks into Higher-Order Logic, Antoine Martina, Alexander Steen. Journal of Logic and Computation
• An Escape from Vardanyan’s Theorem, Ana de Almeida Borges, Joost J. Joosten, JSL
• 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
• Asynchronous Modal FRP, Patrick Bahr, Rasmus Ejlers Møgelberg, ICFP’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
• Automated generation of illustrated proofs in geometry and beyond, Predrag Janičić, Julien Narboux, Annals of Mathematics and Artificial Intelligence, [AMAI]
• Automatic Program Instrumentation for Automatic Verification, Jesper Amilon, Zafer Esen, Dilian Gurov, Christian Lidström, Philipp Rümmer, CAV’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
• Certified Core-Guided MaxSAT Solving, Jeremias Berg, Bart Bogaerts, Jakob Nordström, Andy Oertel, Dieter Vandesande, CADE’23
• Certified Dominance and Symmetry Breaking for Combinatorial Optimisation, Bart Bogaerts, Stephan Gocht, Ciaran McCreesh, Jakob Nordström, JAIR’23
• Challenges for Non-Classical Reasoning in Contemporary AI Applications, Alexander Steen, Christoph Benzmüller, KI – Künstliche Intelligenz
• CICM’22 System Entries, P. Koepke, A. Lorenzen, B. Shminke, CICM’22
• 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
• Considerations on Approaches and Metrics in Automated Theorem Generation/Finding in Geometry., Pedro Quaresma, Pierluigi Graziani, Stefano M. Nicoletti. ADG 2023
• Currying Order and Restricted Algorithmic Beta-Conversion in Type Theory of Acyclic Recursion, Roussanka Loukanova, Logically Speaking. A Festschrift for Marie Duzi
• Decidability of Difference Logic over the Reals with Uninterpreted Unary Predicates, Bernard Boigelot, Pascal Fontaine, Baptiste Vergain. CADE 2023: 542-559
• Decision Procedures for Sequence Theories, Artur Jež, Anthony Lin, Oliver Markgraf, Philipp Rümmer, CAV’23
• 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
• 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, JAR
• Formalizing Functions as Processes, Beniamino Accattoli, Horace Blanc, Claudio Sacerdoti Coen ITP’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
• 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
• LISA: A Modern Proof System, Simon Guilloud, Sankalp Gambhir, Viktor Kunčak, 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. J. Autom. Reason. 67, 2023
• 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
• 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
• Quantitative Global Memory, Sandra Alves, Delia Kesner, Miguel Ramos, WoLLIC’23
• Radical theory of Scott-open filters, Daniel Misselbeck-Wessel, Peter Schuster, TCS
• Rates of asymptotic regularity for the alternating Halpern-Mann iteration, Laurentiu Leustean, Pedro Pinto, Optimization Letters
• Reasoning about quantifiers in SMT: the QSMA algorithm (Abstract), Maria Paola Bonacina, FMCAD’23
• 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 and Sarah Winkler. Journal of Automated Reasoning, 67(1):6, 42 pages, March 2023
• Semantically-guided goal-sensitive reasoning: decision procedures and the Koala prover, Maria Paola Bonacina, Sarah Winkler, JAR
• Semantics of Propositional Attitudes in Type-Theory of Algorithms, Roussanka Loukanova, LENLS’23
• 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 a geometry deductive database prover., Nuno Baeta, Pedro Quaresma. Ann. Math. Artif. Intell. 91
• Towards an Automatic Proof of the Bakery Algorithm, Aman Goel, Stephan Merz, Karem A. Sakallah, FORTE’23
• Towards an Independent Version of Tarski’s System of Geometry, Pierre Boutry, Stéphane Kastenbaum, Clément Saintier. ADG 2023
• 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

2022

• A Decidable Theory Involving Addition of Differentiable Real Functions, Gabriele Buriola, Domenico Cantone, Giuseppe Cincotti, Eugenio G. Omodeo, Giuseppe T. Spartà, TCS
• 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 post-proceedings
• Adding Dual Variables to Algebraic Reasoning for Gate-Level Multiplier Verification, Daniela Kaufmann, Paul Beame, Armin Biere, Jakob Nordström, DATE’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 Auditable Constraint Programming Solver, Stephan Gocht, Ciaran McCreesh, Jakob Nordström, CP’22
• An extensible equality checking algorithm for dependent type theories, Andrej Bauer, Anja Petkovic Komel, LMCS
• 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 SMT-LIB Theory of Heaps, Zafer Esen, Philipp Rümmer, SMT’22
• 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
• 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
• Certified CNF Translations for Pseudo-Boolean Solving, Stephan Gocht, Ruben Martins, Jakob Nordström, Andy Oertel, SAT’22
• CertiStr: A Certified String Solver, Shuanglong Kan, Anthony Widjaja Lin, Philipp Rümmer, Micha Schrader, CPP’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
• Formal Entity Graphs as Complex Networks: Assessing Centrality Metrics of the Archive of Formal Proofs, Fabian Huch, CICM’22
• Formalising Ordinal Partition Relations Using Isabelle/HOL, Mirna Džamonja, Angeliki Koutsoukou-Argyraki, Lawrence C. Paulson, Experimental Mathematics, Special Issue on Interactive Theorem Proving in Mathematics Research, Volume 31, 2022 - Issue 2, pages 383-400
• 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
• Greatest HITs: Higher inductive types in coinductive definitions via induction under clocks, Magnus Baunsgaard Kristensen, Rasmus Ejlers Møgelberg, Andrea Vezzosi, LICS’22
• Irrationality and Transcendence Criteria for Infinite Series in Isabelle/HOL, Angeliki Koutsoukou-Argyraki, Wenda Li, Lawrence C. Paulson, Experimental Mathematics, Special Issue on Interactive Theorem Proving in Mathematics Research
• 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
• Logic Operators and Quantifiers in Type-Theory of Algorithms, Roussanka Loukanova, LENLS 2022
• 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
• Re-imagining the Isabelle Archive of Formal Proofs, MacKenzie, C., Huch, F., Vaughan, J., Fleuriot, CICM’22
• 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
• Tricera: Verifying C Programs Using the Theory of Heaps, Zafer Esen, Philipp Rümmer, FMCAD’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

• 3rd WG3 meeting, Dresden, 27-28 March, 2024, slides&videos report
• 2nd WG3 meeting, Timisoara, 8-9 February 2023, slides&videos report
• 1st WG3 meeting, Valencia, 10-11 February 2022 slides&videos report