| Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
| 1 | Pierre-Léo Bégay, Pierre Crégut, Jean-François Monin |
Developing and certifying Datalog optimizations in coq/mathcomp.  |
CPP  |
2021 |
DBLP DOI BibTeX RDF |
|
| 1 | Alexander Lochmann, Aart Middeldorp, Fabian Mitterwallner, Bertram Felgenhauer |
A verified decision procedure for the first-order theory of rewriting for linear variable-separated rewrite systems. |
CPP |
2021 |
DBLP DOI BibTeX RDF |
|
| 1 | Jonas Kastberg Hinrichsen, Daniël Louwrink, Robbert Krebbers, Jesper Bengtson |
Machine-checked semantic session typing. |
CPP |
2021 |
DBLP DOI BibTeX RDF |
|
| 1 | Amin Timany, Lars Birkedal |
Reasoning about monotonicity in separation logic. |
CPP |
2021 |
DBLP DOI BibTeX RDF |
|
| 1 | Magnus O. Myreen |
A minimalistic verified bootstrapped compiler (proof pearl). |
CPP |
2021 |
DBLP DOI BibTeX RDF |
|
| 1 | Yannick Zakowski, Paul He, Chung-Kil Hur, Steve Zdancewic |
An equational theory for weak bisimulation via generalized parameterized coinduction. |
CPP |
2020 |
DBLP DOI BibTeX RDF |
|
| 1 | Danil Annenkov, Jakob Botsch Nielsen, Bas Spitters |
ConCert: a smart contract certification framework in Coq. |
CPP |
2020 |
DBLP DOI BibTeX RDF |
|
| 1 | Niccolò Veltri, Andrea Vezzosi |
Formalizing π-calculus in guarded cubical Agda. |
CPP |
2020 |
DBLP DOI BibTeX RDF |
|
| 1 | Simon Spies, Yannick Forster 0002 |
Undecidability of higher-order unification formalised in Coq. |
CPP |
2020 |
DBLP DOI BibTeX RDF |
|
| 1 | Abhishek Kr Singh, Raja Natarajan |
A constructive formalization of the weak perfect graph theorem. |
CPP |
2020 |
DBLP DOI BibTeX RDF |
|
| 1 | Clement Blaudeau, Natarajan Shankar |
A verified packrat parser interpreter for parsing expression grammars. |
CPP |
2020 |
DBLP DOI BibTeX RDF |
|
| 1 | Yannick Forster 0002, Kathrin Stark |
Coq à la carte: a practical approach to modular syntax with binders. |
CPP |
2020 |
DBLP DOI BibTeX RDF |
|
| 1 | |
The lean mathematical library. |
CPP |
2020 |
DBLP DOI BibTeX RDF |
|
| 1 | Tobias Nipkow, Thomas Sewell |
Proof pearl: Braun trees. |
CPP |
2020 |
DBLP DOI BibTeX RDF |
|
| 1 | Anders Mörtberg, Loïc Pujet |
Cubical synthetic homotopy theory. |
CPP |
2020 |
DBLP DOI BibTeX RDF |
|
| 1 | Johannes Altmanninger, Adrian Rebola-Pardo |
Frying the egg, roasting the chicken: unit deletions in DRAT proofs. |
CPP |
2020 |
DBLP DOI BibTeX RDF |
|
| 1 | Grigore Rosu, Xiaohong Chen 0002 |
Matching logic: the foundation of the K framework (invited talk). |
CPP |
2020 |
DBLP DOI BibTeX RDF |
|
| 1 | Adam Chlipala |
Proof assistants at the hardware-software interface (invited talk). |
CPP |
2020 |
DBLP DOI BibTeX RDF |
|
| 1 | Tomás Díaz, Federico Olmedo, Éric Tanter |
A mechanized formalization of GraphQL. |
CPP |
2020 |
DBLP DOI BibTeX RDF |
|
| 1 | Qingxiang Wang, Chad E. Brown, Cezary Kaliszyk, Josef Urban |
Exploration of neural machine translation in autoformalization of mathematics in Mizar. |
CPP |
2020 |
DBLP DOI BibTeX RDF |
|
| 1 | Roy Overbeek |
Formalizing determinacy of concurrent revisions. |
CPP |
2020 |
DBLP DOI BibTeX RDF |
|
| 1 | Fredrik Nordvall Forsberg, Chuangjie Xu, Neil Ghani |
Three equivalent ordinal notation systems in cubical Agda. |
CPP |
2020 |
DBLP DOI BibTeX RDF |
|
| 1 | Talia Ringer, Alex Sanchez-Stern, Dan Grossman, Sorin Lerner |
REPLica: REPL instrumentation for Coq analysis. |
CPP |
2020 |
DBLP DOI BibTeX RDF |
|
| 1 | Fabian Immler, Yong Kiam Tan |
The Poincaré-Bendixson theorem in Isabelle/HOL. |
CPP |
2020 |
DBLP DOI BibTeX RDF |
|
| 1 | Jasmin Blanchette, Catalin Hritcu (eds.) |
Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, New Orleans, LA, USA, January 20-21, 2020. |
CPP |
2020 |
DBLP DOI BibTeX RDF |
|
| 1 | Yannick Forster 0002, Fabian Kunze, Maxi Wuttke |
Verified programming of Turing machines in Coq. |
CPP |
2020 |
DBLP DOI BibTeX RDF |
|
| 1 | Arjen Rouvoet, Casper Bach Poulsen, Robbert Krebbers, Eelco Visser |
Intrinsically-typed definitional interpreters for linear, session-typed languages. |
CPP |
2020 |
DBLP DOI BibTeX RDF |
|
| 1 | Jesse Michael Han, Floris van Doorn |
A formal proof of the independence of the continuum hypothesis. |
CPP |
2020 |
DBLP DOI BibTeX RDF |
|
| 1 | Shilpi Goel, Anna Slobodová, Rob Sumners, Sol Swords |
Verifying x86 instruction implementations. |
CPP |
2020 |
DBLP DOI BibTeX RDF |
|
| 1 | Christian Doczkal, Damien Pous |
Completeness of an axiomatization of graph isomorphism via graph rewriting in Coq. |
CPP |
2020 |
DBLP DOI BibTeX RDF |
|
| 1 | David Butler 0002, David Aspinall 0001, Adrià Gascón |
Formalising oblivious transfer in the semi-honest and malicious model in CryptHOL. |
CPP |
2020 |
DBLP DOI BibTeX RDF |
|
| 1 | Thomas Letan, Yann Régis-Gianas |
FreeSpec: specifying, verifying, and executing impure computations in Coq. |
CPP |
2020 |
DBLP DOI BibTeX RDF |
|
| 1 | Denis Firsov, Ahto Buldas, Ahto Truu, Risto Laanoja |
Verified security of BLT signature scheme. |
CPP |
2020 |
DBLP DOI BibTeX RDF |
|
| 1 | Kevin Buzzard, Johan Commelin, Patrick Massot |
Formalising perfectoid spaces. |
CPP |
2020 |
DBLP DOI BibTeX RDF |
|
| 1 | Linh Tran, Anshuman Mohan, Aquinas Hobor |
A functional proof pearl: inverting the Ackermann hierarchy. |
CPP |
2020 |
DBLP DOI BibTeX RDF |
|
| 1 | Qianchuan Ye, Benjamin Delaware |
A verified protocol buffer compiler. |
CPP |
2019 |
DBLP DOI BibTeX RDF |
|
| 1 | Susannah Mansky, Elsa L. Gunter |
Dynamic class initialization semantics: a jinja extension. |
CPP |
2019 |
DBLP DOI BibTeX RDF |
|
| 1 | Yannick Forster 0002, Steven Schäfer, Simon Spies, Kathrin Stark |
Call-by-push-value in coq: operational, equational, and denotational theory. |
CPP |
2019 |
DBLP DOI BibTeX RDF |
|
| 1 | Ian Roessle, Freek Verbeek, Binoy Ravindran |
Formally verified big step semantics out of x86-64 binaries. |
CPP |
2019 |
DBLP DOI BibTeX RDF |
|
| 1 | Anders Schlichtkrull, Jasmin Christian Blanchette, Dmitriy Traytel |
A verified prover based on ordered resolution. |
CPP |
2019 |
DBLP DOI BibTeX RDF |
|
| 1 | Sandrine Blazy, Rémi Hutin |
Formal verification of a program obfuscation based on mixed Boolean-arithmetic expressions. |
CPP |
2019 |
DBLP DOI BibTeX RDF |
|
| 1 | Yannick Forster 0002, Dominik Kirst, Gert Smolka |
On synthetic undecidability in coq, with an application to the entscheidungsproblem. |
CPP |
2019 |
DBLP DOI BibTeX RDF |
|
| 1 | Assia Mahboubi, Magnus O. Myreen (eds.) |
Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2019, Cascais, Portugal, January 14-15, 2019 |
CPP |
2019 |
DBLP BibTeX RDF |
|
| 1 | Amy P. Felty |
A linear logical framework in hybrid (invited talk). |
CPP |
2019 |
DBLP DOI BibTeX RDF |
|
| 1 | Nicolas Koh, Yao Li 0004, Yishuai Li, Li-yao Xia, Lennart Beringer, Wolf Honoré, William Mansky, Benjamin C. Pierce, Steve Zdancewic |
From C to interaction trees: specifying, verifying, and testing a networked server. |
CPP |
2019 |
DBLP DOI BibTeX RDF |
|
| 1 | Yannick Forster 0002, Dominique Larchey-Wendling |
Certified undecidability of intuitionistic linear logic via binary stack machines and minsky machines. |
CPP |
2019 |
DBLP DOI BibTeX RDF |
|
| 1 | Théo Winterhalter, Matthieu Sozeau, Nicolas Tabareau |
Eliminating reflection from type theory. |
CPP |
2019 |
DBLP DOI BibTeX RDF |
|
| 1 | Wenda Li, Lawrence C. Paulson |
Counting polynomial roots in isabelle/hol: a formal proof of the budan-fourier theorem. |
CPP |
2019 |
DBLP DOI BibTeX RDF |
|
| 1 | Bertram Felgenhauer, Aart Middeldorp, T. V. H. Prathamesh, Franziska Rapp |
A verified ground confluence tool for linear variable-separated rewrite systems in Isabelle/HOL. |
CPP |
2019 |
DBLP DOI BibTeX RDF |
|
| 1 | Véronique Benzaken, Evelyne Contejean |
A Coq mechanised formal semantics for realistic SQL queries: formally reconciling SQL and bag relational algebra. |
CPP |
2019 |
DBLP DOI BibTeX RDF |
|
| 1 | Jasmin Christian Blanchette |
Formalizing the metatheory of logical calculi and automatic provers in Isabelle/HOL (invited talk). |
CPP |
2019 |
DBLP DOI BibTeX RDF |
|
| 1 | Kathrin Stark, Steven Schäfer, Jonas Kaiser |
Autosubst 2: reasoning with multi-sorted de Bruijn terms and vector substitutions. |
CPP |
2019 |
DBLP DOI BibTeX RDF |
|
| 1 | Fabian Immler, Bohua Zhan |
Smooth manifolds and types to sets for linear algebra in Isabelle/HOL. |
CPP |
2019 |
DBLP DOI BibTeX RDF |
|
| 1 | Kaustuv Chaudhuri, Matteo Manighetti, Dale Miller 0001 |
A proof-theoretic approach to certifying skolemization. |
CPP |
2019 |
DBLP DOI BibTeX RDF |
|
| 1 | Alexander Lochmann, Christian Sternagel |
Certified ACKBO. |
CPP |
2019 |
DBLP DOI BibTeX RDF |
|
| 1 | Manuel Eberl |
Verified solving and asymptotics of linear recurrences. |
CPP |
2019 |
DBLP DOI BibTeX RDF |
|
| 1 | Robert Y. Lewis |
A formal proof of hensel's lemma over the p-adic integers. |
CPP |
2019 |
DBLP DOI BibTeX RDF |
|
| 1 | Kaustuv Chaudhuri |
A two-level logic perspective on (simultaneous) substitutions. |
CPP |
2018 |
DBLP DOI BibTeX RDF |
|
| 1 | Cezary Kaliszyk, Julian Parsert |
Formal microeconomic foundations and the first welfare theorem. |
CPP |
2018 |
DBLP DOI BibTeX RDF |
|
| 1 | Hugo Férée, Samuel Hym, Micaela Mayero, Jean-Yves Moyen, David Nowak |
Formal proof of polynomial-time complexity with quasi-interpretations. |
CPP |
2018 |
DBLP DOI BibTeX RDF |
|
| 1 | Pawel Wieczorek, Dariusz Biernacki |
A Coq formalization of normalization by evaluation for Martin-Löf type theory. |
CPP |
2018 |
DBLP DOI BibTeX RDF |
|
| 1 | Boris Djalal |
A constructive formalisation of Semi-algebraic sets and functions. |
CPP |
2018 |
DBLP DOI BibTeX RDF |
|
| 1 | Maria Paola Bonacina, Stéphane Graham-Lengrand, Natarajan Shankar |
Proofs in conflict-driven theory combination. |
CPP |
2018 |
DBLP DOI BibTeX RDF |
|
| 1 | Niklas Grimm, Kenji Maillard, Cédric Fournet, Catalin Hritcu, Matteo Maffei, Jonathan Protzenko, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy, Santiago Zanella Béguelin |
A monadic framework for relational verification: applied to information security, program equivalence, and optimizations. |
CPP |
2018 |
DBLP DOI BibTeX RDF |
|
| 1 | Sidney Amani, Myriam Bégel, Maksym Bortin, Mark Staples |
Towards verifying ethereum smart contract bytecode in Isabelle/HOL. |
CPP |
2018 |
DBLP DOI BibTeX RDF |
|
| 1 | Damien Rouhling |
A formal proof in Coq of a control function for the inverted pendulum. |
CPP |
2018 |
DBLP DOI BibTeX RDF |
|
| 1 | Eric Mullen, Stuart Pernsteiner, James R. Wilcox, Zachary Tatlock, Dan Grossman |
Œuf: minimizing the Coq extraction TCB. |
CPP |
2018 |
DBLP DOI BibTeX RDF |
|
| 1 | Sergueï Lenglet, Alan Schmitt |
HOπ in Coq. |
CPP |
2018 |
DBLP DOI BibTeX RDF |
|
| 1 | Dan Frumin, Herman Geuvers, Léon Gondelman, Niels van der Weide |
Finite sets in homotopy type theory. |
CPP |
2018 |
DBLP DOI BibTeX RDF |
|
| 1 | Craig McLaughlin, James McKinna, Ian Stark |
Triangulating context lemmas. |
CPP |
2018 |
DBLP DOI BibTeX RDF |
|
| 1 | Christian Doczkal, Joachim Bard |
Completeness and decidability of converse PDL in the constructive type theory of Coq. |
CPP |
2018 |
DBLP DOI BibTeX RDF |
|
| 1 | Jonas Kaiser, Steven Schäfer, Kathrin Stark |
Binder aware recursion over well-scoped de Bruijn syntax. |
CPP |
2018 |
DBLP DOI BibTeX RDF |
|
| 1 | Talia Ringer, Nathaniel Yazdani, John Leo, Dan Grossman |
Adapting proof automation to adapt proofs. |
CPP |
2018 |
DBLP DOI BibTeX RDF |
|
| 1 | Mathias Fleury, Jasmin Christian Blanchette, Peter Lammich |
A verified SAT solver with watched literals using imperative HOL. |
CPP |
2018 |
DBLP DOI BibTeX RDF |
|
| 1 | Jose Divasón, Sebastiaan J. C. Joosten, Ondrej Kuncar, René Thiemann, Akihisa Yamada 0002 |
Efficient certification of complexity proofs: formalizing the Perron-Frobenius theorem (invited talk paper). |
CPP |
2018 |
DBLP DOI BibTeX RDF |
|
| 1 | Brigitte Pientka |
POPLMark reloaded: mechanizing logical relations proofs (invited talk). |
CPP |
2018 |
DBLP DOI BibTeX RDF |
|
| 1 | June Andronick, Amy P. Felty (eds.) |
Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2018, Los Angeles, CA, USA, January 8-9, 2018 |
CPP |
2018 |
DBLP BibTeX RDF |
|
| 1 | Dominik Kirst, Gert Smolka |
Large model constructions for second-order ZF in dependent type theory. |
CPP |
2018 |
DBLP DOI BibTeX RDF |
|
| 1 | Denis Firsov, Aaron Stump |
Generic derivation of induction for impredicative encodings in Cedille. |
CPP |
2018 |
DBLP DOI BibTeX RDF |
|
| 1 | Conrad Watt |
Mechanising and verifying the WebAssembly specification. |
CPP |
2018 |
DBLP DOI BibTeX RDF |
|
| 1 | George Pîrlea, Ilya Sergey |
Mechanising blockchain consensus. |
CPP |
2018 |
DBLP DOI BibTeX RDF |
|
| 1 | Antal Spector-Zabusky, Joachim Breitner, Christine Rizkallah, Stephanie Weirich |
Total Haskell is reasonable Coq. |
CPP |
2018 |
DBLP DOI BibTeX RDF |
|
| 1 | Rose Bohrer, Vincent Rahli, Ivana Vukotic, Marcus Völp, André Platzer |
Formally verified differential dynamic logic. |
CPP |
2017 |
DBLP DOI BibTeX RDF |
|
| 1 | Johannes Hölzl |
Markov processes in Isabelle/HOL. |
CPP |
2017 |
DBLP DOI BibTeX RDF |
|
| 1 | Xinyu Feng 0001 |
Mechanized verification of preemptive OS kernels (invited talk). |
CPP |
2017 |
DBLP DOI BibTeX RDF |
|
| 1 | Jose Divasón, Sebastiaan J. C. Joosten, René Thiemann, Akihisa Yamada 0002 |
A formalization of the Berlekamp-Zassenhaus factorization algorithm. |
CPP |
2017 |
DBLP DOI BibTeX RDF |
|
| 1 | Lawrence C. Paulson |
Porting the HOL light analysis library: some lessons (invited talk). |
CPP |
2017 |
DBLP DOI BibTeX RDF |
|
| 1 | Sidney Amani, June Andronick, Maksym Bortin, Corey Lewis, Christine Rizkallah, Joseph Tuong |
Complx: a verification framework for concurrent imperative programs. |
CPP |
2017 |
DBLP DOI BibTeX RDF |
|
| 1 | William Mansky, Yuanfeng Peng, Steve Zdancewic, Joseph Devietti |
Verifying dynamic race detection. |
CPP |
2017 |
DBLP DOI BibTeX RDF |
|
| 1 | Yves Bertot, Viktor Vafeiadis (eds.) |
Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017, Paris, France, January 16-17, 2017 |
CPP |
2017 |
DBLP DOI BibTeX RDF |
|
| 1 | Reynald Affeldt, Cyril Cohen |
Formal foundations of 3D geometry to model robot manipulators. |
CPP |
2017 |
DBLP DOI BibTeX RDF |
|
| 1 | Andrej Bauer, Jason Gross, Peter LeFanu Lumsdaine, Michael Shulman, Matthieu Sozeau, Bas Spitters |
The HoTT library: a formalization of homotopy type theory in Coq. |
CPP |
2017 |
DBLP DOI BibTeX RDF |
|
| 1 | Érik Martin-Dorel, Pierre Roux |
A reflexive tactic for polynomial positivity using numerical solvers and floating-point computations. |
CPP |
2017 |
DBLP DOI BibTeX RDF |
|
| 1 | François Pottier |
Verifying a hash table and its iterators in higher-order separation logic. |
CPP |
2017 |
DBLP DOI BibTeX RDF |
|
| 1 | Gaëtan Gilbert |
Formalising real numbers in homotopy type theory. |
CPP |
2017 |
DBLP DOI BibTeX RDF |
|
| 1 | Jonas Kaiser, Tobias Tebbi, Gert Smolka |
Equivalence of system f and ź2 in Coq based on context morphism lemmas. |
CPP |
2017 |
DBLP DOI BibTeX RDF |
|
| 1 | Simon Boulier, Pierre-Marie Pédrot, Nicolas Tabareau |
The next 700 syntactical models of type theory. |
CPP |
2017 |
DBLP DOI BibTeX RDF |
|
| 1 | Jan Jakubuv, Josef Urban |
BliStrTune: hierarchical invention of theorem proving strategies. |
CPP |
2017 |
DBLP DOI BibTeX RDF |
|
| 1 | Guillaume Allais, James Chapman 0001, Conor McBride, James McKinna |
Type-and-scope safe programs and their proofs. |
CPP |
2017 |
DBLP DOI BibTeX RDF |
|
| 1 | Anthony C. J. Fox, Magnus O. Myreen, Yong Kiam Tan, Ramana Kumar |
Verified compilation of CakeML to multiple machine-code targets. |
CPP |
2017 |
DBLP DOI BibTeX RDF |
|
![[Valid RSS]](Pics/valid-rss.png "Validate my RSS feed")
data released under the ODC-BY 1.0 license