Search results for "CPP"

Hits ?▲	Authors	Title	Venue	Year	Link
44	Victor Cacciari Miraldo, Harold Carr, Mark Moir, Lisandra Silva, Guy L. Steele Jr.	Formal verification of authenticated, append-only skip lists in Agda.	CPP	2021	DBLP DOI BibTeX RDF
44	Dominik Kirst, Felix Rech	The generalised continuum hypothesis implies the axiom of choice in Coq.	CPP	2021	DBLP DOI BibTeX RDF
44	Jannis Limperg	A novice-friendly induction tactic for lean.	CPP	2021	DBLP DOI BibTeX RDF
44	Johan Commelin, Robert Y. Lewis	Formalizing the ring of Witt vectors.	CPP	2021	DBLP DOI BibTeX RDF
44	Andreas Lööw	Lutsig: a verified Verilog compiler for verified circuit development.	CPP	2021	DBLP DOI BibTeX RDF
44	Max W. Haslbeck, René Thiemann	An Isabelle/HOL formalization of AProVE's termination method for LLVM IR.	CPP	2021	DBLP DOI BibTeX RDF
44	Sophie Tourret, Jasmin Blanchette	A modular Isabelle framework for verifying saturation provers.	CPP	2021	DBLP DOI BibTeX RDF
44	Jason Z. S. Hu, Jacques Carette	Formalizing category theory in Agda.	CPP	2021	DBLP DOI BibTeX RDF
44	Simon Friis Vindum, Lars Birkedal	Contextual refinement of the Michael-Scott queue (proof pearl).	CPP	2021	DBLP DOI BibTeX RDF
44	J. Tanner Slagel, Lauren White, Aaron Dutle	Formal verification of semi-algebraic sets and real analytic functions.	CPP	2021	DBLP DOI BibTeX RDF
44	Olivier Laurent 0001	An anti-locally-nameless approach to formalizing quantifiers.	CPP	2021	DBLP DOI BibTeX RDF
44	Joseph Tassarotti, Koundinya Vajjha, Anindya Banerjee 0001, Jean-Baptiste Tristan	A formal proof of PAC learnability for decision stumps.	CPP	2021	DBLP DOI BibTeX RDF
44	Koundinya Vajjha, Avraham Shinnar, Barry M. Trager, Vasily Pestun, Nathan Fulton	CertRL: formalizing convergence proofs for value and policy iteration in Coq.	CPP	2021	DBLP DOI BibTeX RDF
44	Danil Annenkov, Mikkel Milo, Jakob Botsch Nielsen, Bas Spitters	Extracting smart contracts tested and verified in Coq.	CPP	2021	DBLP DOI BibTeX RDF
44	Peter Sewell	Underpinning the foundations: sail-based semantics, testing, and reasoning for production and CHERI-enabled architectures (invited talk).	CPP	2021	DBLP DOI BibTeX RDF
44	Heiko Becker, Nathaniel Bos, Ivan Gavran, Eva Darulova, Rupak Majumdar	Lassie: HOL4 tactics by example.	CPP	2021	DBLP DOI BibTeX RDF
44	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
44	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
44	Jonas Kastberg Hinrichsen, Daniël Louwrink, Robbert Krebbers, Jesper Bengtson	Machine-checked semantic session typing.	CPP	2021	DBLP DOI BibTeX RDF
44	Amin Timany, Lars Birkedal	Reasoning about monotonicity in separation logic.	CPP	2021	DBLP DOI BibTeX RDF
44	Magnus O. Myreen	A minimalistic verified bootstrapped compiler (proof pearl).	CPP	2021	DBLP DOI BibTeX RDF
44	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
44	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
44	Danil Annenkov, Jakob Botsch Nielsen, Bas Spitters	ConCert: a smart contract certification framework in Coq.	CPP	2020	DBLP DOI BibTeX RDF
44	Niccolò Veltri, Andrea Vezzosi	Formalizing π-calculus in guarded cubical Agda.	CPP	2020	DBLP DOI BibTeX RDF
44	Simon Spies, Yannick Forster 0002	Undecidability of higher-order unification formalised in Coq.	CPP	2020	DBLP DOI BibTeX RDF
44	Abhishek Kr Singh, Raja Natarajan	A constructive formalization of the weak perfect graph theorem.	CPP	2020	DBLP DOI BibTeX RDF
44	Clement Blaudeau, Natarajan Shankar	A verified packrat parser interpreter for parsing expression grammars.	CPP	2020	DBLP DOI BibTeX RDF
44	Yannick Forster 0002, Kathrin Stark	Coq à la carte: a practical approach to modular syntax with binders.	CPP	2020	DBLP DOI BibTeX RDF
44		The lean mathematical library.	CPP	2020	DBLP DOI BibTeX RDF
44	Tobias Nipkow, Thomas Sewell	Proof pearl: Braun trees.	CPP	2020	DBLP DOI BibTeX RDF
44	Anders Mörtberg, Loïc Pujet	Cubical synthetic homotopy theory.	CPP	2020	DBLP DOI BibTeX RDF
44	Johannes Altmanninger, Adrian Rebola-Pardo	Frying the egg, roasting the chicken: unit deletions in DRAT proofs.	CPP	2020	DBLP DOI BibTeX RDF
44	Grigore Rosu, Xiaohong Chen 0002	Matching logic: the foundation of the K framework (invited talk).	CPP	2020	DBLP DOI BibTeX RDF
44	Adam Chlipala	Proof assistants at the hardware-software interface (invited talk).	CPP	2020	DBLP DOI BibTeX RDF
44	Tomás Díaz, Federico Olmedo, Éric Tanter	A mechanized formalization of GraphQL.	CPP	2020	DBLP DOI BibTeX RDF
44	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
44	Roy Overbeek	Formalizing determinacy of concurrent revisions.	CPP	2020	DBLP DOI BibTeX RDF
44	Fredrik Nordvall Forsberg, Chuangjie Xu, Neil Ghani	Three equivalent ordinal notation systems in cubical Agda.	CPP	2020	DBLP DOI BibTeX RDF
44	Talia Ringer, Alex Sanchez-Stern, Dan Grossman, Sorin Lerner	REPLica: REPL instrumentation for Coq analysis.	CPP	2020	DBLP DOI BibTeX RDF
44	Fabian Immler, Yong Kiam Tan	The Poincaré-Bendixson theorem in Isabelle/HOL.	CPP	2020	DBLP DOI BibTeX RDF
44	Yannick Forster 0002, Fabian Kunze, Maxi Wuttke	Verified programming of Turing machines in Coq.	CPP	2020	DBLP DOI BibTeX RDF
44	Arjen Rouvoet, Casper Bach Poulsen, Robbert Krebbers, Eelco Visser	Intrinsically-typed definitional interpreters for linear, session-typed languages.	CPP	2020	DBLP DOI BibTeX RDF
44	Jesse Michael Han, Floris van Doorn	A formal proof of the independence of the continuum hypothesis.	CPP	2020	DBLP DOI BibTeX RDF
44	Shilpi Goel, Anna Slobodová, Rob Sumners, Sol Swords	Verifying x86 instruction implementations.	CPP	2020	DBLP DOI BibTeX RDF
44	Christian Doczkal, Damien Pous	Completeness of an axiomatization of graph isomorphism via graph rewriting in Coq.	CPP	2020	DBLP DOI BibTeX RDF
44	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
44	Thomas Letan, Yann Régis-Gianas	FreeSpec: specifying, verifying, and executing impure computations in Coq.	CPP	2020	DBLP DOI BibTeX RDF
44	Denis Firsov, Ahto Buldas, Ahto Truu, Risto Laanoja	Verified security of BLT signature scheme.	CPP	2020	DBLP DOI BibTeX RDF
44	Kevin Buzzard, Johan Commelin, Patrick Massot	Formalising perfectoid spaces.	CPP	2020	DBLP DOI BibTeX RDF
44	Linh Tran, Anshuman Mohan, Aquinas Hobor	A functional proof pearl: inverting the Ackermann hierarchy.	CPP	2020	DBLP DOI BibTeX RDF
44	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
44	Qianchuan Ye, Benjamin Delaware	A verified protocol buffer compiler.	CPP	2019	DBLP DOI BibTeX RDF
44	Susannah Mansky, Elsa L. Gunter	Dynamic class initialization semantics: a jinja extension.	CPP	2019	DBLP DOI BibTeX RDF
44	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
44	Ian Roessle, Freek Verbeek, Binoy Ravindran	Formally verified big step semantics out of x86-64 binaries.	CPP	2019	DBLP DOI BibTeX RDF
44	Anders Schlichtkrull, Jasmin Christian Blanchette, Dmitriy Traytel	A verified prover based on ordered resolution.	CPP	2019	DBLP DOI BibTeX RDF
44	Sandrine Blazy, Rémi Hutin	Formal verification of a program obfuscation based on mixed Boolean-arithmetic expressions.	CPP	2019	DBLP DOI BibTeX RDF
44	Yannick Forster 0002, Dominik Kirst, Gert Smolka	On synthetic undecidability in coq, with an application to the entscheidungsproblem.	CPP	2019	DBLP DOI BibTeX RDF
44	Amy P. Felty	A linear logical framework in hybrid (invited talk).	CPP	2019	DBLP DOI BibTeX RDF
44	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
44	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
44	Théo Winterhalter, Matthieu Sozeau, Nicolas Tabareau	Eliminating reflection from type theory.	CPP	2019	DBLP DOI BibTeX RDF
44	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
44	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
44	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
44	Jasmin Christian Blanchette	Formalizing the metatheory of logical calculi and automatic provers in Isabelle/HOL (invited talk).	CPP	2019	DBLP DOI BibTeX RDF
44	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
44	Fabian Immler, Bohua Zhan	Smooth manifolds and types to sets for linear algebra in Isabelle/HOL.	CPP	2019	DBLP DOI BibTeX RDF
44	Kaustuv Chaudhuri, Matteo Manighetti, Dale Miller 0001	A proof-theoretic approach to certifying skolemization.	CPP	2019	DBLP DOI BibTeX RDF
44	Alexander Lochmann, Christian Sternagel	Certified ACKBO.	CPP	2019	DBLP DOI BibTeX RDF
44	Manuel Eberl	Verified solving and asymptotics of linear recurrences.	CPP	2019	DBLP DOI BibTeX RDF
44	Robert Y. Lewis	A formal proof of hensel's lemma over the p-adic integers.	CPP	2019	DBLP DOI BibTeX RDF
44	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
44	Kaustuv Chaudhuri	A two-level logic perspective on (simultaneous) substitutions.	CPP	2018	DBLP DOI BibTeX RDF
44	Cezary Kaliszyk, Julian Parsert	Formal microeconomic foundations and the first welfare theorem.	CPP	2018	DBLP DOI BibTeX RDF
44	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
44	Pawel Wieczorek, Dariusz Biernacki	A Coq formalization of normalization by evaluation for Martin-Löf type theory.	CPP	2018	DBLP DOI BibTeX RDF
44	Boris Djalal	A constructive formalisation of Semi-algebraic sets and functions.	CPP	2018	DBLP DOI BibTeX RDF
44	Maria Paola Bonacina, Stéphane Graham-Lengrand, Natarajan Shankar	Proofs in conflict-driven theory combination.	CPP	2018	DBLP DOI BibTeX RDF
44	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
44	Sidney Amani, Myriam Bégel, Maksym Bortin, Mark Staples	Towards verifying ethereum smart contract bytecode in Isabelle/HOL.	CPP	2018	DBLP DOI BibTeX RDF
44	Damien Rouhling	A formal proof in Coq of a control function for the inverted pendulum.	CPP	2018	DBLP DOI BibTeX RDF
44	Eric Mullen, Stuart Pernsteiner, James R. Wilcox, Zachary Tatlock, Dan Grossman	Œuf: minimizing the Coq extraction TCB.	CPP	2018	DBLP DOI BibTeX RDF
44	Sergueï Lenglet, Alan Schmitt	HOπ in Coq.	CPP	2018	DBLP DOI BibTeX RDF
44	Dan Frumin, Herman Geuvers, Léon Gondelman, Niels van der Weide	Finite sets in homotopy type theory.	CPP	2018	DBLP DOI BibTeX RDF
44	Craig McLaughlin, James McKinna, Ian Stark	Triangulating context lemmas.	CPP	2018	DBLP DOI BibTeX RDF
44	Christian Doczkal, Joachim Bard	Completeness and decidability of converse PDL in the constructive type theory of Coq.	CPP	2018	DBLP DOI BibTeX RDF
44	Jonas Kaiser, Steven Schäfer, Kathrin Stark	Binder aware recursion over well-scoped de Bruijn syntax.	CPP	2018	DBLP DOI BibTeX RDF
44	Talia Ringer, Nathaniel Yazdani, John Leo, Dan Grossman	Adapting proof automation to adapt proofs.	CPP	2018	DBLP DOI BibTeX RDF
44	Mathias Fleury, Jasmin Christian Blanchette, Peter Lammich	A verified SAT solver with watched literals using imperative HOL.	CPP	2018	DBLP DOI BibTeX RDF
44	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
44	Brigitte Pientka	POPLMark reloaded: mechanizing logical relations proofs (invited talk).	CPP	2018	DBLP DOI BibTeX RDF
44	Dominik Kirst, Gert Smolka	Large model constructions for second-order ZF in dependent type theory.	CPP	2018	DBLP DOI BibTeX RDF
44	Denis Firsov, Aaron Stump	Generic derivation of induction for impredicative encodings in Cedille.	CPP	2018	DBLP DOI BibTeX RDF
44	Conrad Watt	Mechanising and verifying the WebAssembly specification.	CPP	2018	DBLP DOI BibTeX RDF
44	George Pîrlea, Ilya Sergey	Mechanising blockchain consensus.	CPP	2018	DBLP DOI BibTeX RDF
44	Antal Spector-Zabusky, Joachim Breitner, Christine Rizkallah, Stephanie Weirich	Total Haskell is reasonable Coq.	CPP	2018	DBLP DOI BibTeX RDF
44	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
44	Rose Bohrer, Vincent Rahli, Ivana Vukotic, Marcus Völp, André Platzer	Formally verified differential dynamic logic.	CPP	2017	DBLP DOI BibTeX RDF