researchr
explore
Tags
Journals
Conferences
Authors
Profiles
Groups
calendar
New Conferences
Events
Deadlines
search
search
You are not signed in
Sign in
Sign up
Links
Filter by Year
OR
AND
NOT
1
2010
2011
2012
2013
2014
2015
2016
2017
2018
2019
2021
2022
2023
2024
2025
Filter by Tag
[+]
OR
AND
NOT
1
algebra
C++
Java
Meta-Environment
abstract syntax
analysis
architecture
case study
compiler
consistency
context-aware
discovery
graph-rewriting
logic
program verification
proof assistant
rewriting
rule-based
semantics
termination
Filter by Author
[+]
OR
AND
NOT
1
Andreas Lochbihler
Andrei Popescu 0001
Assia Mahboubi
Cezary Kaliszyk
Christian Urban
Cyril Cohen
Dmitriy Traytel
Enrico Tassi
Gert Smolka
Gerwin Klein
Jasmin Christian Blanchette
Jeremy Avigad
Johannes Hölzl
Josef Urban
Magnus O. Myreen
Michael Norrish
Peter Lammich
Ramana Kumar
Reynald Affeldt
Tobias Nipkow
Filter by Top terms
[+]
OR
AND
NOT
1
algorithm
conference
coq
formal
formalization
formalizing
higher
hol
interactive
isabelle
logic
order
proof
proofs
proving
theorem
theory
using
verification
verified
ITP (itp)
Editions
Publications
Viewing Publication 1 - 100 from 564
2025
16th International Conference on Interactive Theorem Proving, ITP 2025, September 28 to October 1, 2025, Reykjavik, Iceland
Yannick Forster 0001
,
Chantal Keller
, editors,
Volume 352 of
LIPIcs
, Schloss Dagstuhl - Leibniz-Zentrum für Informatik,
2025.
[doi]
An Isabelle/HOL Formalization of Semi-Thue and Conditional Semi-Thue Systems
Dohan Kim 0001
.
itp 2025
:
[doi]
Mechanising Böhm Trees and λη-Completeness
Chun Tian 0001
,
Michael Norrish
.
itp 2025
:
[doi]
Front Matter, Table of Contents, Preface, Conference Organization
itp 2025
:
[doi]
A Formal Analysis of Algorithms for Matroids and Greedoids
Mohammad Abdulaziz
,
Thomas Ammer
,
Shriya Meenakshisundaram
,
Adem Rimpapa
.
itp 2025
:
[doi]
Formalizing Concentration Inequalities in Rocq: Infrastructure and Automation
Reynald Affeldt
,
Alessandro Bruni
,
Cyril Cohen
,
Pierre Roux 0001
,
Takafumi Saikawa
.
itp 2025
:
[doi]
A Formal Proof of Complexity Bounds on Diophantine Equations
Jonas Bayer
,
Marco David
.
itp 2025
:
[doi]
Formalizing Splitting in Isabelle/HOL
Ghilain Bergeron
,
Florent Krasnopol
,
Sophie Tourret
.
itp 2025
:
[doi]
Formally Verifying a Vertical Cell Decomposition Algorithm
Yves Bertot
,
Thomas Portet
.
itp 2025
:
[doi]
Formalizing the Hidden Number Problem in Isabelle/HOL
Sage Binder
,
Eric Ren
,
Katherine Kosaian
.
itp 2025
:
[doi]
Program Optimisations via Hylomorphisms for Extraction of Executable Code
David Castro-Perez
,
Marco Paviotti
,
Michael Vollmer 0003
.
itp 2025
:
[doi]
A Formalization of Divided Powers in Lean
Antoine Chambert-Loir
,
María Inés de Frutos-Fernández
.
itp 2025
:
[doi]
A Verified Cost Model for Call-By-Push-Value
Zhuo Zoey Chen
,
Johannes Åman Pohjola
,
Christine Rizkallah
.
itp 2025
:
[doi]
A Mechanized First-Order Theory of Algebraic Data Types with Pattern Matching
Joshua M. Cohen
.
itp 2025
:
[doi]
Formalising Inductive and Coinductive Containers
Stefania Damato
,
Thorsten Altenkirch
,
Axel Ljungström
.
itp 2025
:
[doi]
Sledgehammering Without ATPs (Short Paper)
Martin Desharnais
,
Jasmin Blanchette
.
itp 2025
:
[doi]
A Certified Proof Checker for Deep Neural Network Verification in Imandra
Remi Desmartin
,
Omri Isac
,
Grant O. Passmore
,
Ekaterina Komendantskaya
,
Kathrin Stark
,
Guy Katz
.
itp 2025
:
[doi]
Verifying an Efficient Algorithm for Computing Bernoulli Numbers
Manuel Eberl
,
Peter Lammich
.
itp 2025
:
[doi]
Formalising Subject Reduction and Progress for Multiparty Session Processes
Burak Ekici
,
Tadayoshi Kamegai
,
Nobuko Yoshida
.
itp 2025
:
[doi]
Abstract, Compositional Consistency: Isabelle/HOL Locales for Completeness à la Fitting
Asta Halkjær From
,
Anders Schlichtkrull
.
itp 2025
:
[doi]
Automatically Generalizing Proofs and Statements
Anshula Gandhi
,
Anand Rao Tadipatri
,
Timothy Gowers
.
itp 2025
:
[doi]
Towards Automating Permutation Proofs in Rocq: A Reflexive Approach with Iterative Deepening Search (Short Paper)
Nadeem Abdul Hamid
.
itp 2025
:
[doi]
Verification of the CVM Algorithm with a Functional Probabilistic Invariant
Emin Karayel
,
Seng Joe Watt
,
Derek Khu
,
Kuldeep S. Meel
,
Yong Kiam Tan
.
itp 2025
:
[doi]
On Verifying Secret Control Flow Elimination
David Knothe
,
Oliver Bringmann 0001
.
itp 2025
:
[doi]
A Natural Language Formalization of Perfectoid Rings in ℕaproche
Peter Koepke
.
itp 2025
:
[doi]
Inductive Predicates via Least Fixpoints in Higher-Order Separation Logic
Robbert Krebbers
,
Luko van der Maas
,
Enrico Tassi
.
itp 2025
:
[doi]
Improving the SMT Proof Reconstruction Pipeline in Isabelle/HOL
Hanna Lachnitt
,
Mathias Fleury
,
Haniel Barbosa
,
Jibiana Jakpor
,
Bruno Andreotti
,
Andrew Reynolds 0001
,
Hans-Jörg Schurr
,
Clark W. Barrett
,
Cesare Tinelli
.
itp 2025
:
[doi]
Barendregt's Theory of the λ-Calculus, Refreshed and Formalized
Adrienne Lancelot
,
Beniamino Accattoli
,
Maxime Vemclefs
.
itp 2025
:
[doi]
Certified Implementability of Global Multiparty Protocols
Elaine Li
,
Thomas Wies
.
itp 2025
:
[doi]
GOL in GOL in HOL: Verified Circuits in Conway's Game of Life
Magnus O. Myreen
,
Mario Carneiro
.
itp 2025
:
[doi]
Canonical for Automated Theorem Proving in Lean
Chase Norman
,
Jeremy Avigad
.
itp 2025
:
[doi]
Formalising New Mathematics in Isabelle: Diagonal Ramsey
Lawrence C. Paulson
.
itp 2025
:
[doi]
Nondeterministic Asynchronous Dataflow in Isabelle/HOL
Rafael Castro Gonçalves Silva
,
Laouen Fernet
,
Dmitriy Traytel
.
itp 2025
:
[doi]
Autosubst: On Mechanising Binders in a General-Purpose Proof Assistant (Invited Talk)
Kathrin Stark
.
itp 2025
:
[doi]
Verifying Datalog Reasoning with Lean
Johannes Tantow
,
Lukas Gerlach 0002
,
Stephan Mennicke
,
Markus Krötzsch
.
itp 2025
:
[doi]
Nanopass Back-Translation of Call-Return Trees for Mechanized Secure Compilation Proofs
Jérémy Thibault
,
Joseph Lenormand
,
Catalin Hritcu
.
itp 2025
:
[doi]
Taming Floating-Point Rounding Errors with Proofs (Invited Talk)
Laura Titolo
.
itp 2025
:
[doi]
Animating MRBNFs: Truly Modular Binding-Aware Datatypes in Isabelle/HOL
Jan van Brügge
,
Andrei Popescu 0001
,
Dmitriy Traytel
.
itp 2025
:
[doi]
Scott's Representation Theorem and the Univalent Karoubi Envelope
Arnoud van der Leer
,
Kobe Wullaert
,
Benedikt Ahrens
.
itp 2025
:
[doi]
LeanLTL: A Unifying Framework for Linear Temporal Logics in Lean (Short Paper)
Eric Vin
,
Kyle A. Miller
,
Daniel J. Fremont
.
itp 2025
:
[doi]
Algebra Is Half the Battle: Verifying Presentations of Graded Unipotent Chevalley Groups
Eric Wang
,
Arohee Bhoja
,
Cayden R. Codel
,
Noah G. Singer
.
itp 2025
:
[doi]
Finiteness of Symbolic Derivatives in Lean
Ekaterina Zhuchko
,
Hendrik Maarand
,
Margus Veanes
,
Gabriel Ebner
.
itp 2025
:
[doi]
2024
An Isabelle/HOL Formalization of Narrowing and Multiset Narrowing for E-Unifiability, Reachability and Infeasibility
Dohan Kim 0001
.
itp 2024
:
[doi]
A Coq Formalization of Taylor Models and Power Series for Solving Ordinary Differential Equations
Sewon Park 0001
,
Holger Thies
.
itp 2024
:
[doi]
Front Matter, Table of Contents, Preface, Conference Organization
itp 2024
:
[doi]
A Formal Analysis of Capacity Scaling Algorithms for Minimum Cost Flows
Mohammad Abdulaziz
,
Thomas Ammer
.
itp 2024
:
[doi]
A Comprehensive Overview of the Lebesgue Differentiation Theorem in Coq
Reynald Affeldt
,
Zachary Stone
.
itp 2024
:
[doi]
Taming Differentiable Logics with Coq Formalisation
Reynald Affeldt
,
Alessandro Bruni
,
Ekaterina Komendantskaya
,
Natalia Slusarz
,
Kathrin Stark
.
itp 2024
:
[doi]
Robust Mean Estimation by All Means (Short Paper)
Reynald Affeldt
,
Clark W. Barrett
,
Alessandro Bruni
,
Ieva Daukantas
,
Harun Khan
,
Takafumi Saikawa
,
Carsten Schürmann
.
itp 2024
:
[doi]
Towards Solid Abelian Groups: A Formal Proof of Nöbeling's Theorem
Dagur Asgeirsson
.
itp 2024
:
[doi]
An Operational Semantics in Isabelle/HOL-CSP
Benoît Ballenghien
,
Burkhart Wolff
.
itp 2024
:
[doi]
The Directed Van Kampen Theorem in Lean
Henning Basold
,
Peter Bruin
,
Dominique Lawson
.
itp 2024
:
[doi]
15th International Conference on Interactive Theorem Proving, ITP 2024, September 9-14, 2024, Tbilisi, Georgia
Yves Bertot
,
Temur Kutsia
,
Michael Norrish
, editors,
Volume 309 of
LIPIcs
, Schloss Dagstuhl - Leibniz-Zentrum für Informatik,
2024.
[doi]
Verifying Peephole Rewriting in SSA Compiler IRs
Siddharth Bhat
,
Alex C. Keizer
,
Chris Hughes
,
Andrés Goens
,
Tobias Grosser
.
itp 2024
:
[doi]
Translating Libraries of Definitions and Theorems Between Proof Systems (Invited Talk)
Frédéric Blanqui
.
itp 2024
:
[doi]
Duper: A Proof-Producing Superposition Theorem Prover for Dependent Type Theory
Joshua Clune
,
Yicheng Qian
,
Alexander Bentkamp
,
Jeremy Avigad
.
itp 2024
:
[doi]
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 2024
:
[doi]
A Modular Formalization of Superposition in Isabelle/HOL
Martin Desharnais
,
Balázs Tóth
,
Uwe Waldmann
,
Jasmin Blanchette
,
Sophie Tourret
.
itp 2024
:
[doi]
Formalising Half of a Graduate Textbook on Number Theory (Short Paper)
Manuel Eberl
,
Anthony Bordg
,
Lawrence C. Paulson
,
Wenda Li
.
itp 2024
:
[doi]
Completeness of Asynchronous Session Tree Subtyping in Coq
Burak Ekici
,
Nobuko Yoshida
.
itp 2024
:
[doi]
Graphical Rewriting for Diagrammatic Reasoning in Monoidal Categories in Lean4 (Short Paper)
Sam Ezeh
.
itp 2024
:
[doi]
End-To-End Formal Verification of a Fast and Accurate Floating-Point Approximation
Florian Faissole
,
Paul Geneau de Lamarlière
,
Guillaume Melquiond
.
itp 2024
:
[doi]
Typed Compositional Quantum Computation with Lenses
Jacques Garrigue
,
Takafumi Saikawa
.
itp 2024
:
[doi]
A Formal Proof of R(4, 5)=25
Thibault Gauthier
,
Chad E. Brown
.
itp 2024
:
[doi]
Verifying Software Emulation of an Unsupported Hardware Instruction
Samuel Gruetter
,
Thomas Bourgeat
,
Adam Chlipala
.
itp 2024
:
[doi]
Mechanized HOL Reasoning in Set Theory
Simon Guilloud
,
Sankalp Gambhir
,
Andrea Gilot
,
Viktor Kuncak
.
itp 2024
:
[doi]
Modular Verification of Intrusive List and Tree Data Structures in Separation Logic
Marc Hermes
,
Robbert Krebbers
.
itp 2024
:
[doi]
Formalizing the Algebraic Small Object Argument in UniMath
Dennis Hilhorst
,
Paige Randall North
.
itp 2024
:
[doi]
A Formalization of the Lévy-Prokhorov Metric in Isabelle/HOL
Michikazu Hirata
.
itp 2024
:
[doi]
Distributed Parallel Build for the Isabelle Archive of Formal Proofs
Fabian Huch
,
Makarius Wenzel
.
itp 2024
:
[doi]
A Generalised Union of Rely-Guarantee and Separation Logic Using Permission Algebras
Vincent Jackson
,
Toby Murray
,
Christine Rizkallah
.
itp 2024
:
[doi]
Formalizing the Cholesky Factorization Theorem
Carl Kwan
,
Warren A. Hunt Jr.
.
itp 2024
:
[doi]
The Rewster: Type Preserving Rewrite Rules for the Coq Proof Assistant
Yann Leray
,
Gaëtan Gilbert
,
Nicolas Tabareau
,
Théo Winterhalter
.
itp 2024
:
[doi]
Teaching Mathematics Using Lean and Controlled Natural Language
Patrick Massot
.
itp 2024
:
[doi]
Alpha-Beta Pruning Verified (Invited Talk)
Tobias Nipkow
.
itp 2024
:
[doi]
Lean Formalization of Completeness Proof for Coalition Logic with Common Knowledge
Kai Obendrauf
,
Anne Baanen
,
Patrick Koopmann
,
Vera Stebletsova
.
itp 2024
:
[doi]
Conway Normal Form: Bridging Approaches for Comprehensive Formalization of Surreal Numbers
Karol Pak
,
Cezary Kaliszyk
.
itp 2024
:
[doi]
A Verified Earley Parser
Martin Rau
,
Tobias Nipkow
.
itp 2024
:
[doi]
Abstractions for Multi-Sorted Substitutions
Hannes Saffrich
.
itp 2024
:
[doi]
Correctly Compiling Proofs About Programs Without Proving Compilers Correct
Audrey Seo
,
Christopher Lam 0003
,
Dan Grossman
,
Talia Ringer
.
itp 2024
:
[doi]
Redex2Coq: Towards a Theory of Decidability of Redex's Reduction Semantics
Mallku Soldevila
,
Rodrigo Geraldo Ribeiro
,
Beta Ziliani
.
itp 2024
:
[doi]
Formal Verification of the Empty Hexagon Number
Bernardo Subercaseaux
,
Wojciech Nawrocki
,
James Gallicchio
,
Cayden R. Codel
,
Mario Carneiro
,
Marijn J. H. Heule
.
itp 2024
:
[doi]
Defining and Preserving More C Behaviors: Verified Compilation Using a Concrete Memory Model
Andrew Tolmach
,
Chris Chhak
,
Sean Noble Anderson
.
itp 2024
:
[doi]
Integrals Within Integrals: A Formalization of the Gagliardo-Nirenberg-Sobolev Inequality
Floris van Doorn
,
Heather Macbeth
.
itp 2024
:
[doi]
The Functor of Points Approach to Schemes in Cubical Agda
Max Zeuner
,
Matthias Hutzler
.
itp 2024
:
[doi]
2023
Front Matter, Table of Contents, Preface, Conference Organization
itp 2023
:
[doi]
An Elementary Formal Proof of the Group Law on Weierstrass Elliptic Curves in Any Characteristic
David Kurniadi Angdinata
,
Junyan Xu
.
itp 2023
:
[doi]
Reimplementing Mizar in Rust
Mario Carneiro
.
itp 2023
:
[doi]
Formalizing Norm Extensions and Applications to Number Theory
María Inés de Frutos-Fernández
.
itp 2023
:
[doi]
Formalising Yoneda Ext in Univalent Foundations
Jarl G. Taxerås Flaten
.
itp 2023
:
[doi]
Semantic Foundations of Higher-Order Probabilistic Programs in Isabelle/HOL
Michikazu Hirata
,
Yasuhiko Minamide
,
Tetsuya Sato 0001
.
itp 2023
:
[doi]
Constructive Final Semantics of Finite Bags
Philipp Joram
,
Niccolò Veltri
.
itp 2023
:
[doi]
Formalizing Almost Development Closed Critical Pairs (Short Paper)
Christina Kohl
,
Aart Middeldorp
.
itp 2023
:
[doi]
Group Cohomology in the Lean Community Library
Amelia Livingston
.
itp 2023
:
[doi]
A Formalisation of Gallagher's Ergodic Theorem
Oliver Nash
.
itp 2023
:
[doi]
Bel-Games: A Formal Theory of Games of Incomplete Information Based on Belief Functions in the Coq Proof Assistant
Pierre Pomeret-Coquot
,
Hélène Fargier
,
Érik Martin-Dorel
.
itp 2023
:
[doi]
A Sound and Complete Projection for Global Types
Dawit Legesse Tirore
,
Jesper Bengtson
,
Marco Carbone
.
itp 2023
:
[doi]
Real-Time Double-Ended Queue Verified (Proof Pearl)
Balázs Tóth
,
Tobias Nipkow
.
itp 2023
:
[doi]
Certifying Higher-Order Polynomial Interpretations
Niels van der Weide
,
Deivid Vale
,
Cynthia Kop
.
itp 2023
:
[doi]
Formalising the Proj Construction in Lean
Jujian Zhang
.
itp 2023
:
[doi]
Sign in
or
sign up
to see more results.