default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDSearch dblp
Full-text search
- > Home
Please enter a search query
- case-insensitive prefix search: default
e.g., sig matches "SIGIR" as well as "signal" - exact word search: append dollar sign ($) to word
e.g., graph$ matches "graph", but not "graphics" - boolean and: separate words by space
e.g., codd model - boolean or: connect words by pipe symbol (|)
e.g., graph|network
Update May 7, 2017: Please note that we had to disable the phrase search operator (.) and the boolean not operator (-) due to technical problems. For the time being, phrase search queries will yield regular prefix search result, and search terms preceded by a minus will be interpreted as regular (positive) search terms.
Author search results
no matches
Venue search results
no matches
Refine list
refine by author
- no options
- temporarily not available
refine by venue
- no options
- temporarily not available
refine by type
- no options
- temporarily not available
refine by access
- no options
- temporarily not available
refine by year
- no options
- temporarily not available
Publication search results
found 499 matches
- 2024
- Dohan Kim:
An Isabelle/HOL Formalization of Narrowing and Multiset Narrowing for E-Unifiability, Reachability and Infeasibility. ITP 2024: 24:1-24:19 - Sewon Park, Holger Thies:
A Coq Formalization of Taylor Models and Power Series for Solving Ordinary Differential Equations. ITP 2024: 30:1-30:19 - Mohammad Abdulaziz
, Thomas Ammer:
A Formal Analysis of Capacity Scaling Algorithms for Minimum Cost Flows. ITP 2024: 3:1-3:19 - Reynald Affeldt, Clark W. Barrett, Alessandro Bruni, Ieva Daukantas, Harun Khan, Takafumi Saikawa, Carsten Schürmann:
Robust Mean Estimation by All Means (Short Paper). ITP 2024: 39:1-39:8 - Reynald Affeldt, Alessandro Bruni, Ekaterina Komendantskaya, Natalia Slusarz, Kathrin Stark:
Taming Differentiable Logics with Coq Formalisation. ITP 2024: 4:1-4:19 - Reynald Affeldt, Zachary Stone:
A Comprehensive Overview of the Lebesgue Differentiation Theorem in Coq. ITP 2024: 5:1-5:19 - Dagur Asgeirsson:
Towards Solid Abelian Groups: A Formal Proof of Nöbeling's Theorem. ITP 2024: 6:1-6:17 - Benoît Ballenghien, Burkhart Wolff:
An Operational Semantics in Isabelle/HOL-CSP. ITP 2024: 7:1-7:18 - Henning Basold, Peter Bruin, Dominique Lawson:
The Directed Van Kampen Theorem in Lean. ITP 2024: 8:1-8:18 - Siddharth Bhat, Alex C. Keizer, Chris Hughes, Andrés Goens, Tobias Grosser:
Verifying Peephole Rewriting in SSA Compiler IRs. ITP 2024: 9:1-9:20 - Frédéric Blanqui:
Translating Libraries of Definitions and Theorems Between Proof Systems (Invited Talk). ITP 2024: 2:1-2:1 - Joshua Clune, Yicheng Qian, Alexander Bentkamp, Jeremy Avigad:
Duper: A Proof-Producing Superposition Theorem Prover for Dependent Type Theory. ITP 2024: 10:1-10:20 - Martin Desharnais, Balázs Tóth, Uwe Waldmann, Jasmin Blanchette, Sophie Tourret:
A Modular Formalization of Superposition in Isabelle/HOL. ITP 2024: 12:1-12:20 - Floris van Doorn, Heather Macbeth:
Integrals Within Integrals: A Formalization of the Gagliardo-Nirenberg-Sobolev Inequality. ITP 2024: 37:1-37:18 - Manuel Eberl, Anthony Bordg, Lawrence C. Paulson, Wenda Li:
Formalising Half of a Graduate Textbook on Number Theory (Short Paper). ITP 2024: 40:1-40:7 - Burak Ekici, Nobuko Yoshida:
Completeness of Asynchronous Session Tree Subtyping in Coq. ITP 2024: 13:1-13:20 - Sam Ezeh:
Graphical Rewriting for Diagrammatic Reasoning in Monoidal Categories in Lean4 (Short Paper). ITP 2024: 41:1-41:8 - Florian Faissole, Paul Geneau de Lamarlière, Guillaume Melquiond:
End-To-End Formal Verification of a Fast and Accurate Floating-Point Approximation. ITP 2024: 14:1-14:18 - Jacques Garrigue, Takafumi Saikawa:
Typed Compositional Quantum Computation with Lenses. ITP 2024: 15:1-15:18 - Thibault Gauthier, Chad E. Brown:
A Formal Proof of R(4, 5)=25. ITP 2024: 16:1-16:18 - Samuel Gruetter, Thomas Bourgeat, Adam Chlipala:
Verifying Software Emulation of an Unsupported Hardware Instruction. ITP 2024: 17:1-17:16 - Simon Guilloud, Sankalp Gambhir, Andrea Gilot, Viktor Kuncak:
Mechanized HOL Reasoning in Set Theory. ITP 2024: 18:1-18:18 - Marc Hermes, Robbert Krebbers:
Modular Verification of Intrusive List and Tree Data Structures in Separation Logic. ITP 2024: 19:1-19:18 - Dennis Hilhorst, Paige Randall North:
Formalizing the Algebraic Small Object Argument in UniMath. ITP 2024: 20:1-20:18 - Michikazu Hirata:
A Formalization of the Lévy-Prokhorov Metric in Isabelle/HOL. ITP 2024: 21:1-21:18 - Fabian Huch, Makarius Wenzel:
Distributed Parallel Build for the Isabelle Archive of Formal Proofs. ITP 2024: 22:1-22:19 - Vincent Jackson, Toby Murray, Christine Rizkallah:
A Generalised Union of Rely-Guarantee and Separation Logic Using Permission Algebras. ITP 2024: 23:1-23:16 - Carl Kwan, Warren A. Hunt Jr.:
Formalizing the Cholesky Factorization Theorem. ITP 2024: 25:1-25:16 - Yann Leray, Gaëtan Gilbert, Nicolas Tabareau, Théo Winterhalter:
The Rewster: Type Preserving Rewrite Rules for the Coq Proof Assistant. ITP 2024: 26:1-26:18 - Thaynara Arielly de Lima, André Luiz Galdino, Bruno Berto de Oliveira Ribeiro, Mauricio Ayala-Rincón:
A Formalization of the General Theory of Quaternions. ITP 2024: 11:1-11:18
skipping 469 more matches
loading more results 
failed to load more results, please try again later
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from 
to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the 
of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from 
, 
, and 
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from 
.
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
retrieved on 2024-11-26 00:51 CET from data curated by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
