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
2025
- Scalable Knowledge Refactoring using Constrained Optimisation, Minghao Liu, David M. Cerna, Filipe Gouveia, Andrew Cropper. AAAI’25
- A Predicative Approach to the Constructive Integration Theory of Locally Compact Metric Spaces, Fabian Lukas Grubmüller, Iosif Petrakis. J. Log. Anal.
- 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
2024
- 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 Matroid-Based Automatic Prover and Coq Proof Generator for Projective Incidence Geometry, David Braun, NicolasMagaud, 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
- 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.
- 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
- Certifying Incremental SAT Solving, Katalin Fazekas, Florian Pollitt, Mathias Fleury, Armin Biere. LPAR’24
- Comodule Representations of Second-Order Functionals, Danel Ahman, Andrej Bauer
- Complemented Subsets and Boolean-valued, Partial Functions, Daniel Misselbeck-Wessel, Iosif Petrakis, Comput.
- Differentiable Inductive Logic Programming in High-Dimensional Space, Stanisław J. Purgał, David M. Cerna, Cezary Kaliszyk. IJCLR’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
- 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
- Isabelle-Verified Correctness of Datalog Programs for Program Analysis, Anders Schlichtkrull, René Rydhof Hansen, Flemming Nielson. SAC’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
- 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
- Orthologic with Axioms, Simon Guilloud, Viktor Kunčak. POPL’24
- Pre-measure Spaces and Pre-integration Spaces in Predicative Bishop-Cheng Measure Theory, Iosif Petrakis, Max Zeuner. LMCS
- Proof-carrying Parameters in Certified Symbolic Execution, Andrei Arusoaie, Dorel Lucanu, LJIGPL
- Proofs for Free in the λΠ-Calculus Modulo Theory, Thomas Traversié, LFMTP’24
- Reasoning in Transformers - Mitigating Spurious Correlations and Reasoning Shortcuts, Daniel Enström, Viktor Kjellberg, Moa Johansson. NeSy’24
- SC-TPTP: An Extension of the TPTP Derivation Format for Sequent-Based Calculus, Julie Cailler, Simon Guilloud. PAAR’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
- Sets Completely Separated by Functions in Bishop Set Theory, Iosif Petrakis. Notre Dame J. Formal Logic
- Shared Terms and Cached Rewriting, Stephan Schulz. IWIL’24
- Sharing proofs with predicative theories through universe-polymorphic elaboration, Thiago Felicissimo, Frédéric Blanqui, LMCS
- Specify What? Enhancing Neural Specification Synthesis by Symbolic Methods, George Granberry, Wolfgang Ahrendt, Moa Johansson, IFM’24
- 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 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 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
- Towards the Exact Complexity of Realizability for Safety LTL, Noel Arteche, Montserrat Hermo, JLAMP
- 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
- Who finds the short proof?, Christoph Benzmüller, David Fuenmayor, Alexander Steen, Geoff Sutcliffe. LJIGPL
2023
- A Formalisation of the Balog-Szemerédi-Gowers Theorem in Isabelle/HOL, Angeliki Koutsoukou-Argyraki, Mantas Bakšys and Chelsea Edmonds. CPP ’23
- 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
- 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
- CICM’22 System Entries, P. Koepke, A. Lorenzen, B. Shminke. CICM’22
- 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
- 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
- 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
- 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
- Quantitative Global Memory, Sandra Alves, Delia Kesner, Miguel Ramos. WoLLIC’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
- 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 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
2022
- Formal Entity Graphs as Complex Networks: Assessing Centrality Metrics of the Archive of Formal Proofs, Fabian Huch. CICM’22
- Re-imagining the Isabelle Archive of Formal Proofs, MacKenzie, C., Huch, F., Vaughan, J., Fleuriot. CICM’22
- 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
- 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
- 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
- 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
- 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