The FacetedDBLP logo    Search for: in:

Disable automatic phrases ?     Syntactic query expansion: ?

Publications at "ITP"( http://dblp.L3S.de/Venues/ITP )

URL (DBLP): http://dblp.uni-trier.de/db/conf/itp

Publication years (Num. hits)
2010 (36) 2011 (30) 2012 (30) 2013 (39) 2014 (38) 2015 (31) 2016 (33) 2017 (33) 2018 (39) 2019 (38) 2021 (34) 2022 (35) 2023 (40)
Publication types (Num. hits)
inproceedings(443) proceedings(13)
Venues (Conferences, Journals, ...)
ITP(456)
GrowBag graphs for keyword ? (Num. hits/coverage)

Group by:
No Growbag Graphs found.

Results
Found 456 publication records. Showing 456 according to the selection in the facets
Hits ? Authors Title Venue Year Link Author keywords
1Amelia Livingston Group Cohomology in the Lean Community Library. Search on Bibsonomy ITP The full citation details ... 2023 DBLP  DOI  BibTeX  RDF
1Dominique Larchey-Wendling, Jean-François Monin Proof Pearl: Faithful Computation and Extraction of μ-Recursive Algorithms in Coq. Search on Bibsonomy ITP The full citation details ... 2023 DBLP  DOI  BibTeX  RDF
1 Front Matter, Table of Contents, Preface, Conference Organization. Search on Bibsonomy ITP The full citation details ... 2023 DBLP  DOI  BibTeX  RDF
1Martin Dvorak, Jasmin Blanchette Closure Properties of General Grammars - Formally Verified. Search on Bibsonomy ITP The full citation details ... 2023 DBLP  DOI  BibTeX  RDF
1Alex J. Best, Christopher Birkbeck, Riccardo Brasca, Eric Rodriguez Boidi Fermat's Last Theorem for Regular Primes (Short Paper). Search on Bibsonomy ITP The full citation details ... 2023 DBLP  DOI  BibTeX  RDF
1María Inés de Frutos-Fernández Formalizing Norm Extensions and Applications to Number Theory. Search on Bibsonomy ITP The full citation details ... 2023 DBLP  DOI  BibTeX  RDF
1Jujian Zhang Formalising the Proj Construction in Lean. Search on Bibsonomy ITP The full citation details ... 2023 DBLP  DOI  BibTeX  RDF
1Angeliki Koutsoukou-Argyraki Formalisation of Additive Combinatorics in Isabelle/HOL (Invited Talk). Search on Bibsonomy ITP The full citation details ... 2023 DBLP  DOI  BibTeX  RDF
1Michikazu Hirata, Yasuhiko Minamide, Tetsuya Sato 0001 Semantic Foundations of Higher-Order Probabilistic Programs in Isabelle/HOL. Search on Bibsonomy ITP The full citation details ... 2023 DBLP  DOI  BibTeX  RDF
1Beniamino Accattoli, Horace Blanc, Claudio Sacerdoti Coen Formalizing Functions as Processes. Search on Bibsonomy ITP The full citation details ... 2023 DBLP  DOI  BibTeX  RDF
1Adam Grabowski, Artur Kornilowicz Implementing More Explicit Definitional Expansions in Mizar (Short Paper). Search on Bibsonomy ITP The full citation details ... 2023 DBLP  DOI  BibTeX  RDF
1Yiming Xu, Michael Norrish Dependently Sorted Theorem Proving for Mathematical Foundations. Search on Bibsonomy ITP The full citation details ... 2023 DBLP  DOI  BibTeX  RDF
1Tom Reichel, R. Wesley Henderson, Andrew Touchet, Andrew Gardner, Talia Ringer Proof Repair Infrastructure for Supervised Models: Building a Large Proof Repair Dataset. Search on Bibsonomy ITP The full citation details ... 2023 DBLP  DOI  BibTeX  RDF
1David Kurniadi Angdinata, Junyan Xu An Elementary Formal Proof of the Group Law on Weierstrass Elliptic Curves in Any Characteristic. Search on Bibsonomy ITP The full citation details ... 2023 DBLP  DOI  BibTeX  RDF
1Ana 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 Lessons for Interactive Theorem Proving Researchers from a Survey of Coq Users. Search on Bibsonomy ITP The full citation details ... 2023 DBLP  DOI  BibTeX  RDF
1Wojciech Nawrocki, Edward W. Ayers, Gabriel Ebner An Extensible User Interface for Lean 4. Search on Bibsonomy ITP The full citation details ... 2023 DBLP  DOI  BibTeX  RDF
1Mario Carneiro Reimplementing Mizar in Rust. Search on Bibsonomy ITP The full citation details ... 2023 DBLP  DOI  BibTeX  RDF
1Pierre Pomeret-Coquot, Hélène Fargier, Érik Martin-Dorel Bel-Games: A Formal Theory of Games of Incomplete Information Based on Belief Functions in the Coq Proof Assistant. Search on Bibsonomy ITP The full citation details ... 2023 DBLP  DOI  BibTeX  RDF
1Simon Guilloud, Sankalp Gambhir, Viktor Kuncak LISA - A Modern Proof System. Search on Bibsonomy ITP The full citation details ... 2023 DBLP  DOI  BibTeX  RDF
1Oskar Abrahamsson, Magnus O. Myreen Fast, Verified Computation for Candle. Search on Bibsonomy ITP The full citation details ... 2023 DBLP  DOI  BibTeX  RDF
1Chengsong Tan, Christian Urban POSIX Lexing with Bitcoded Derivatives. Search on Bibsonomy ITP The full citation details ... 2023 DBLP  DOI  BibTeX  RDF
1Christina Kohl, Aart Middeldorp Formalizing Almost Development Closed Critical Pairs (Short Paper). Search on Bibsonomy ITP The full citation details ... 2023 DBLP  DOI  BibTeX  RDF
1Adam Naumowicz, René Thiemann (eds.) 14th International Conference on Interactive Theorem Proving, ITP 2023, July 31 to August 4, 2023, Białystok, Poland Search on Bibsonomy ITP The full citation details ... 2023 DBLP  BibTeX  RDF
1Jan Jakubuv, Karel Chvalovský, Zarathustra Amadeus Goertzel, Cezary Kaliszyk, Mirek Olsák, Bartosz Piotrowski, Stephan Schulz 0001, Martin Suda 0001, Josef Urban MizAR 60 for Mizar 50. Search on Bibsonomy ITP The full citation details ... 2023 DBLP  DOI  BibTeX  RDF
1Niels van der Weide, Deivid Vale, Cynthia Kop Certifying Higher-Order Polynomial Interpretations. Search on Bibsonomy ITP The full citation details ... 2023 DBLP  DOI  BibTeX  RDF
1Dawit Legesse Tirore, Jesper Bengtson, Marco Carbone A Sound and Complete Projection for Global Types. Search on Bibsonomy ITP The full citation details ... 2023 DBLP  DOI  BibTeX  RDF
1Jeremy Avigad, Lior Goldberg, David Levit, Yoav Seginer, Alon Titelman A Proof-Producing Compiler for Blockchain Applications. Search on Bibsonomy ITP The full citation details ... 2023 DBLP  DOI  BibTeX  RDF
1Luís Cruz-Filipe, Fabrizio Montesi Now It Compiles! Certified Automatic Repair of Uncompilable Protocols. Search on Bibsonomy ITP The full citation details ... 2023 DBLP  DOI  BibTeX  RDF
1Jarl G. Taxerås Flaten Formalising Yoneda Ext in Univalent Foundations. Search on Bibsonomy ITP The full citation details ... 2023 DBLP  DOI  BibTeX  RDF
1Oliver Nash A Formalisation of Gallagher's Ergodic Theorem. Search on Bibsonomy ITP The full citation details ... 2023 DBLP  DOI  BibTeX  RDF
1Qinshi Wang, Mengying Pan, Shengyi Wang, Ryan Doenges, Lennart Beringer, Andrew W. Appel Foundational Verification of Stateful P4 Packet Processing. Search on Bibsonomy ITP The full citation details ... 2023 DBLP  DOI  BibTeX  RDF
1Niels F. W. Voorneveld Slice Nondeterminism. Search on Bibsonomy ITP The full citation details ... 2023 DBLP  DOI  BibTeX  RDF
1Philipp Joram, Niccolò Veltri Constructive Final Semantics of Finite Bags. Search on Bibsonomy ITP The full citation details ... 2023 DBLP  DOI  BibTeX  RDF
1Mario Carneiro, Chad E. Brown, Josef Urban Automated Theorem Proving for Metamath. Search on Bibsonomy ITP The full citation details ... 2023 DBLP  DOI  BibTeX  RDF
1Balázs Tóth, Tobias Nipkow Real-Time Double-Ended Queue Verified (Proof Pearl). Search on Bibsonomy ITP The full citation details ... 2023 DBLP  DOI  BibTeX  RDF
1Robbert Krebbers Interactive and Automated Proofs in Modal Separation Logic (Invited Talk). Search on Bibsonomy ITP The full citation details ... 2023 DBLP  DOI  BibTeX  RDF
1Mohammad Abdulaziz, Christoph Madlener A Formal Analysis of RANKING. Search on Bibsonomy ITP The full citation details ... 2023 DBLP  DOI  BibTeX  RDF
1Akihisa Yamada 0002, Jérémy Dubut Formalizing Results on Directed Sets in Isabelle/HOL (Proof Pearl). Search on Bibsonomy ITP The full citation details ... 2023 DBLP  DOI  BibTeX  RDF
1Roger Bosman, Georgios Karachalias, Tom Schrijvers No Unification Variable Left Behind: Fully Grounding Type Inference for the HDM System. Search on Bibsonomy ITP The full citation details ... 2023 DBLP  DOI  BibTeX  RDF
1Lawrence Dunn, Val Tannen, Steve Zdancewic Tealeaves: Structured Monads for Generic First-Order Abstract Syntax Infrastructure. Search on Bibsonomy ITP The full citation details ... 2023 DBLP  DOI  BibTeX  RDF
1Frédéric Dupuis, Robert Y. Lewis, Heather Macbeth Formalized functional analysis with semilinear maps. Search on Bibsonomy ITP The full citation details ... 2022 DBLP  DOI  BibTeX  RDF
1Yury Kudryashov Formalizing the Divergence Theorem and the Cauchy Integral Formula in Lean. Search on Bibsonomy ITP The full citation details ... 2022 DBLP  DOI  BibTeX  RDF
1Nicolas Magaud Proof Pearl: Formalizing Spreads and Packings of the Smallest Projective Space PG(3, 2) Using the Coq Proof Assistant. Search on Bibsonomy ITP The full citation details ... 2022 DBLP  DOI  BibTeX  RDF
1Chelsea Edmonds, Lawrence C. Paulson Formalising Fisher's Inequality: Formal Linear Algebraic Proof Techniques in Combinatorics. Search on Bibsonomy ITP The full citation details ... 2022 DBLP  DOI  BibTeX  RDF
1Dominik Kirst Computational Back-And-Forth Arguments in Constructive Type Theory. Search on Bibsonomy ITP The full citation details ... 2022 DBLP  DOI  BibTeX  RDF
1Oskar Abrahamsson, Magnus O. Myreen, Ramana Kumar, Thomas Sewell Candle: A Verified Implementation of HOL Light. Search on Bibsonomy ITP The full citation details ... 2022 DBLP  DOI  BibTeX  RDF
1Arve Gengelbach, Johannes Åman Pohjola A Verified Cyclicity Checker: For Theories with Overloaded Constants. Search on Bibsonomy ITP The full citation details ... 2022 DBLP  DOI  BibTeX  RDF
1Amy P. Felty Modelling and Verifying Properties of Biological Neural Networks (Invited Talk). Search on Bibsonomy ITP The full citation details ... 2022 DBLP  DOI  BibTeX  RDF
1Malgorzata Biernacka, Witold Charatonik, Tomasz Drab The Zoo of Lambda-Calculus Reduction Strategies, And Coq. Search on Bibsonomy ITP The full citation details ... 2022 DBLP  DOI  BibTeX  RDF
1Hrutvik Kanabar, Anthony C. J. Fox, Magnus O. Myreen Taming an Authoritative Armv8 ISA Specification: L3 Validation and CakeML Compiler Verification. Search on Bibsonomy ITP The full citation details ... 2022 DBLP  DOI  BibTeX  RDF
1Asta Halkjær From, Frederik Krogsdal Jacobsen Verifying a Sequent Calculus Prover for First-Order Logic with Functions in Isabelle/HOL. Search on Bibsonomy ITP The full citation details ... 2022 DBLP  DOI  BibTeX  RDF
1Koundinya Vajjha, Barry M. Trager, Avraham Shinnar, Vasily Pestun Formalization of a Stochastic Approximation Theorem. Search on Bibsonomy ITP The full citation details ... 2022 DBLP  DOI  BibTeX  RDF
1Martin Desharnais, Petar Vukmirovic, Jasmin Blanchette, Makarius Wenzel Seventeen Provers Under the Hammer. Search on Bibsonomy ITP The full citation details ... 2022 DBLP  DOI  BibTeX  RDF
1Anne Baanen Use and Abuse of Instance Parameters in the Lean Mathematical Library. Search on Bibsonomy ITP The full citation details ... 2022 DBLP  DOI  BibTeX  RDF
1Johannes Hostert, Andrej Dudenhefner, Dominik Kirst Undecidability of Dyadic First-Order Logic in Coq. Search on Bibsonomy ITP The full citation details ... 2022 DBLP  DOI  BibTeX  RDF
1Bohua Zhan User Interface Design in the HolPy Theorem Prover (Invited Talk). Search on Bibsonomy ITP The full citation details ... 2022 DBLP  DOI  BibTeX  RDF
1Kazuhiko Sakaguchi Reflexive Tactics for Algebra, Revisited. Search on Bibsonomy ITP The full citation details ... 2022 DBLP  DOI  BibTeX  RDF
1Peter Lammich Refinement of Parallel Algorithms down to LLVM. Search on Bibsonomy ITP The full citation details ... 2022 DBLP  DOI  BibTeX  RDF
1Karol Pak, Cezary Kaliszyk Formalizing a Diophantine Representation of the Set of Prime Numbers. Search on Bibsonomy ITP The full citation details ... 2022 DBLP  DOI  BibTeX  RDF
1Emin Karayel Formalization of Randomized Approximation Algorithms for Frequency Moments. Search on Bibsonomy ITP The full citation details ... 2022 DBLP  DOI  BibTeX  RDF
1Bohua Zhan, Yi Lv, Shuling Wang, Gehang Zhao, Jifeng Hao, Hong Ye, Bican Xia Compositional Verification of Interacting Systems Using Event Monads. Search on Bibsonomy ITP The full citation details ... 2022 DBLP  DOI  BibTeX  RDF
1Alley Stoughton, Carol Chen, Marco Gaboardi, Weihao Qu Formalizing Algorithmic Bounds in the Query Model in EasyCrypt. Search on Bibsonomy ITP The full citation details ... 2022 DBLP  DOI  BibTeX  RDF
1Jason Gross, Théo Zimmermann, Miraya Poddar-Agrawal, Adam Chlipala Automatic Test-Case Reduction in Proof Assistants: A Case Study in Coq. Search on Bibsonomy ITP The full citation details ... 2022 DBLP  DOI  BibTeX  RDF
1Jagadish Bapanapally, Ruben Gamboa A Complete, Mechanically-Verified Proof of the Banach-Tarski Theorem in ACL2(R). Search on Bibsonomy ITP The full citation details ... 2022 DBLP  DOI  BibTeX  RDF
1Heiko Becker, Mohit Tekriwal, Eva Darulova, Anastasia Volkova, Jean-Baptiste Jeannin Dandelion: Certified Approximations of Elementary Functions. Search on Bibsonomy ITP The full citation details ... 2022 DBLP  DOI  BibTeX  RDF
1June Andronick, Leonardo de Moura 0001 (eds.) 13th International Conference on Interactive Theorem Proving, ITP 2022, August 7-10, 2022, Haifa, Israel. Search on Bibsonomy ITP The full citation details ... 2022 DBLP  BibTeX  RDF
1Jared Yeager, J. Eliot B. Moss, Michael Norrish, Philip S. Thomas Mechanizing Soundness of Off-Policy Evaluation. Search on Bibsonomy ITP The full citation details ... 2022 DBLP  DOI  BibTeX  RDF
1Jacob Prinz, G. A. Kavvos, Leonidas Lampropoulos Deeper Shallow Embeddings. Search on Bibsonomy ITP The full citation details ... 2022 DBLP  DOI  BibTeX  RDF
1Yaël Dillies, Bhavik Mehta Formalising Szemerédi's Regularity Lemma in Lean. Search on Bibsonomy ITP The full citation details ... 2022 DBLP  DOI  BibTeX  RDF
1 Front Matter, Table of Contents, Preface, Conference Organization. Search on Bibsonomy ITP The full citation details ... 2022 DBLP  DOI  BibTeX  RDF
1Johannes Åman Pohjola, Alejandro Gómez-Londoño, James Shaker, Michael Norrish Kalas: A Verified, End-To-End Compiler for a Choreographic Language. Search on Bibsonomy ITP The full citation details ... 2022 DBLP  DOI  BibTeX  RDF
1Zarathustra Amadeus Goertzel, Jan Jakubuv, Cezary Kaliszyk, Miroslav Olsák, Jelle Piepenbrock, Josef Urban The Isabelle ENIGMA. Search on Bibsonomy ITP The full citation details ... 2022 DBLP  DOI  BibTeX  RDF
1Yannick Forster 0002, Fabian Kunze, Nils Lauermann Synthetic Kolmogorov Complexity in Coq. Search on Bibsonomy ITP The full citation details ... 2022 DBLP  DOI  BibTeX  RDF
1María Inés de Frutos-Fernández Formalizing the Ring of Adèles of a Global Field. Search on Bibsonomy ITP The full citation details ... 2022 DBLP  DOI  BibTeX  RDF
1Jason Gross, Andres Erbsen, Jade Philipoom, Miraya Poddar-Agrawal, Adam Chlipala Accelerating Verified-Compiler Development with a Verified Rewriting Engine. Search on Bibsonomy ITP The full citation details ... 2022 DBLP  DOI  BibTeX  RDF
1Konrad Slind Specifying Message Formats with Contiguity Types. Search on Bibsonomy ITP The full citation details ... 2021 DBLP  DOI  BibTeX  RDF
1Floris van Doorn Formalized Haar Measure. Search on Bibsonomy ITP The full citation details ... 2021 DBLP  DOI  BibTeX  RDF
1Lennard Gäher, Fabian Kunze Mechanising Complexity Theory: The Cook-Levin Theorem in Coq. Search on Bibsonomy ITP The full citation details ... 2021 DBLP  DOI  BibTeX  RDF
1Matthias Brun 0002, Sára Decova, Andrea Lattuada, Dmitriy Traytel Verified Progress Tracking for Timely Dataflow. Search on Bibsonomy ITP The full citation details ... 2021 DBLP  DOI  BibTeX  RDF
1Christian Doczkal A Variant of Wagner's Theorem Based on Combinatorial Hypermaps. Search on Bibsonomy ITP The full citation details ... 2021 DBLP  DOI  BibTeX  RDF
1Andrei Popescu 0001, Thomas Bauereiss, Peter Lammich Bounded-Deducibility Security (Invited Paper). Search on Bibsonomy ITP The full citation details ... 2021 DBLP  DOI  BibTeX  RDF
1Anne Baanen, Sander R. Dahmen, Ashvni Narayanan, Filippo A. E. Nuccio Mortarino Majno di Capriglio A Formalization of Dedekind Domains and Class Groups of Global Fields. Search on Bibsonomy ITP The full citation details ... 2021 DBLP  DOI  BibTeX  RDF
1Raja Natarajan, Suneel Sarswat, Abhishek Kr Singh Verified Double Sided Auctions for Financial Markets. Search on Bibsonomy ITP The full citation details ... 2021 DBLP  DOI  BibTeX  RDF
1Seulkee Baek A Formally Verified Checker for First-Order Proofs. Search on Bibsonomy ITP The full citation details ... 2021 DBLP  DOI  BibTeX  RDF
1 Front Matter, Table of Contents, Preface, Conference Organization. Search on Bibsonomy ITP The full citation details ... 2021 DBLP  DOI  BibTeX  RDF
1Sophie Bernard, Cyril Cohen, Assia Mahboubi, Pierre-Yves Strub Unsolvability of the Quintic Formalized in Dependent Type Theory. Search on Bibsonomy ITP The full citation details ... 2021 DBLP  DOI  BibTeX  RDF
1Marco Maggesi, Cosimo Perini Brogi A Formal Proof of Modal Completeness for Provability Logic. Search on Bibsonomy ITP The full citation details ... 2021 DBLP  DOI  BibTeX  RDF
1Edward W. Ayers, Mateja Jamnik, William T. Gowers A Graphical User Interface Framework for Formal Verification. Search on Bibsonomy ITP The full citation details ... 2021 DBLP  DOI  BibTeX  RDF
1Christoph Benzmüller, David Fuenmayor Value-Oriented Legal Argumentation in Isabelle/HOL. Search on Bibsonomy ITP The full citation details ... 2021 DBLP  DOI  BibTeX  RDF
1Laurent Théry Proof Pearl : Playing with the Tower of Hanoi Formally. Search on Bibsonomy ITP The full citation details ... 2021 DBLP  DOI  BibTeX  RDF
1Dominik Kirst, Marc Hermes Synthetic Undecidability and Incompleteness of First-Order Axiom Systems in Coq. Search on Bibsonomy ITP The full citation details ... 2021 DBLP  DOI  BibTeX  RDF
1Frédéric Besson Itauto: An Extensible Intuitionistic SAT Solver. Search on Bibsonomy ITP The full citation details ... 2021 DBLP  DOI  BibTeX  RDF
1Hengchu Zhang, Wolf Honoré, Nicolas Koh, Yao Li 0004, Yishuai Li, Li-yao Xia, Lennart Beringer, William Mansky, Benjamin C. Pierce, Steve Zdancewic Verifying an HTTP Key-Value Server with Interaction Trees and VST. Search on Bibsonomy ITP The full citation details ... 2021 DBLP  DOI  BibTeX  RDF
1Nadia Polikarpova Synthesis of Safe Pointer-Manipulating Programs (Invited Talk). Search on Bibsonomy ITP The full citation details ... 2021 DBLP  DOI  BibTeX  RDF
1Yannick Forster 0002, Fabian Kunze, Gert Smolka, Maxi Wuttke A Mechanised Proof of the Time Invariance Thesis for the Weak Call-By-Value λ-Calculus. Search on Bibsonomy ITP The full citation details ... 2021 DBLP  DOI  BibTeX  RDF
1Meven Lennon-Bertrand Complete Bidirectional Typing for the Calculus of Inductive Constructions. Search on Bibsonomy ITP The full citation details ... 2021 DBLP  DOI  BibTeX  RDF
1Joshua Chen Homotopy Type Theory in Isabelle. Search on Bibsonomy ITP The full citation details ... 2021 DBLP  DOI  BibTeX  RDF
1Liron Cohen 0001, Cezary Kaliszyk (eds.) 12th International Conference on Interactive Theorem Proving, ITP 2021, June 29 to July 1, 2021, Rome, Italy (Virtual Conference). Search on Bibsonomy ITP The full citation details ... 2021 DBLP  BibTeX  RDF
1Andreas Lochbihler A Mechanized Proof of the Max-Flow Min-Cut Theorem for Countable Networks. Search on Bibsonomy ITP The full citation details ... 2021 DBLP  DOI  BibTeX  RDF
1Katherine Cordwell, Yong Kiam Tan, André Platzer A Verified Decision Procedure for Univariate Real Arithmetic with the BKR Algorithm. Search on Bibsonomy ITP The full citation details ... 2021 DBLP  DOI  BibTeX  RDF
Displaying result #1 - #100 of 456 (100 per page; Change: )
Pages: [1][2][3][4][5][>>]
Valid XHTML 1.1! Valid CSS! [Valid RSS]
Maintained by L3S.
Previously maintained by Jörg Diederich.
Based upon DBLP by Michael Ley.
open data data released under the ODC-BY 1.0 license