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
2011
2012
2013
2015
2016
2017
2018
2019
2020
2021
2022
2023
2024
Filter by Tag
OR
AND
NOT
1
Intrinsic-Verification
Filter by Author
[+]
OR
AND
NOT
1
Anders Mörtberg
Andrew W. Appel
Bas Spitters
Benjamin Grégoire
Cezary Kaliszyk
Christian Doczkal
Cyril Cohen
Denis Firsov
Dominik Kirst
Gert Smolka
Josef Urban
Kathrin Stark
Kaustuv Chaudhuri
René Thiemann
Robbert Krebbers
Sandrine Blazy
Steven Schäfer
Tahina Ramananandro
Tobias Nipkow
Yannick Forster 0002
Filter by Top terms
[+]
OR
AND
NOT
1
certified
coq
formal
formalization
formalizing
hol
invited
isabelle
logic
programs
proof
proofs
semantics
talk
theorem
theory
type
verification
verified
verifying
CPP (CPP)
Editions
Publications
Viewing Publication 1 - 100 from 318
2024
Martin-Löf à la Coq
Arthur Adjedj
,
Meven Lennon-Bertrand
,
Kenji Maillard
,
Pierre-Marie Pédrot
,
Loïc Pujet
.
CPP 2024
:
230-245
[doi]
Displayed Monoidal Categories for the Semantics of Linear Logic
Benedikt Ahrens
,
Ralph Matthes
,
Niels van der Weide
,
Kobe Wullaert
.
CPP 2024
:
260-273
[doi]
VCFloat2: Floating-Point Error Analysis in Coq
Andrew W. Appel
,
Ariel Kellison
.
CPP 2024
:
14-29
[doi]
PfComp: A Verified Compiler for Packet Filtering Leveraging Binary Decision Diagrams
Clément Chavanon
,
Frédéric Besson
,
Tristan Ninet
.
CPP 2024
:
89-102
[doi]
UTC Time, Formally Verified
Ana de Almeida Borges
,
Mireia González Bedmar
,
Juan José Conejero Rodríguez
,
Eduardo Hermo Reyes
,
Joaquim Casals Buñuel
,
Joost J. Joosten
.
CPP 2024
:
2-13
[doi]
A Formalization of Complete Discrete Valuation Rings and Local Fields
María Inés de Frutos-Fernández
,
Filippo Alberto Edoardo Nuccio Mortarino Majno di Capriglio
.
CPP 2024
:
190-204
[doi]
Formal Probabilistic Methods for Combinatorial Structures using the Lovász Local Lemma
Chelsea Edmonds
,
Lawrence C. Paulson
.
CPP 2024
:
132-146
[doi]
Strictly Monotone Brouwer Trees for Well Founded Recursion over Multiple Arguments
Joseph Eremondi
.
CPP 2024
:
205-217
[doi]
Formalizing Giles Gardam's Disproof of Kaplansky's Unit Conjecture
Siddhartha Gadgil
,
Anand Rao Tadipatri
.
CPP 2024
:
177-189
[doi]
The Last Yard: Foundational End-to-End Verification of High-Speed Cryptography
Philipp G. Haselwarter
,
Benjamin Salling Hvass
,
Lasse Letager Hansen
,
Théo Winterhalter
,
Catalin Hritcu
,
Bas Spitters
.
CPP 2024
:
30-44
[doi]
Certification of Confluence- and Commutation-Proofs via Parallel Critical Pairs
Nao Hirokawa
,
Dohan Kim 0001
,
Kiraku Shintani
,
René Thiemann
.
CPP 2024
:
147-161
[doi]
Formalizing the ∞-Categorical Yoneda Lemma
Nikolai Kudasov
,
Emily Riehl
,
Jonathan Weinberger
.
CPP 2024
:
274-290
[doi]
Memory Simulations, Security and Optimization in a Verified Compiler
David Monniaux
.
CPP 2024
:
103-117
[doi]
Unification for Subformula Linking under Quantifiers
Ike Mulder
,
Robbert Krebbers
.
CPP 2024
:
75-88
[doi]
Compositional Verification of Concurrent C Programs with Search Structure Templates
Duc-Than Nguyen
,
Lennart Beringer
,
William Mansky
,
Shengyi Wang
.
CPP 2024
:
60-74
[doi]
Under-Approximation for Scalable Bug Detection (Keynote)
Azalea Raad
.
CPP 2024
:
1
[doi]
A Mechanised and Constructive Reverse Analysis of Soundness and Completeness of Bi-intuitionistic Logic
Ian Shillito
,
Dominik Kirst
.
CPP 2024
:
218-229
[doi]
Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2024, London, UK, January 15-16, 2024
Amin Timany
,
Dmitriy Traytel
,
Brigitte Pientka
,
Sandrine Blazy
, editors,
ACM,
2024.
[doi]
Univalent Double Categories
Niels van der Weide
,
Nima Rasekh
,
Benedikt Ahrens
,
Paige Randall North
.
CPP 2024
:
246-259
[doi]
A Temporal Differential Dynamic Logic Formal Embedding
Lauren White
,
Laura Titolo
,
J. Tanner Slagel
,
César A. Muñoz
.
CPP 2024
:
162-176
[doi]
Rooting for Efficiency: Mechanised Reasoning about Array-Based Trees in Separation Logic
Qiyuan Zhao
,
George Pîrlea
,
Zhendong Ang
,
Umang Mathur 0001
,
Ilya Sergey
.
CPP 2024
:
45-59
[doi]
Lean Formalization of Extended Regular Expression Matching with Lookarounds
Ekaterina Zhuchko
,
Margus Veanes
,
Gabriel Ebner
.
CPP 2024
:
118-131
[doi]
2023
Terms for Efficient Proof Checking and Parsing
Michael Färber 0002
.
CPP 2023
:
135-147
[doi]
A Computational Cantor-Bernstein and Myhill's Isomorphism Theorem in Constructive Type Theory (Proof Pearl)
Yannick Forster 0002
,
Felix Jahn
,
Gert Smolka
.
CPP 2023
:
159-166
[doi]
Semantics of Probabilistic Programs using s-Finite Kernels in Coq
Reynald Affeldt
,
Cyril Cohen
,
Ayumu Saito
.
CPP 2023
:
3-16
[doi]
A Formal Disproof of Hirsch Conjecture
Xavier Allamigeon
,
Quentin Canu
,
Pierre-Yves Strub
.
CPP 2023
:
17-29
[doi]
FastVer2: A Provably Correct Monitor for Concurrent, Key-Value Stores
Arvind Arasu
,
Tahina Ramananandro
,
Aseem Rastogi
,
Nikhil Swamy
,
Aymeric Fromherz
,
Kesha Hietala
,
Bryan Parno
,
Ravi Ramamurthy
.
CPP 2023
:
30-46
[doi]
A Formalisation of the Balog-Szemerédi-Gowers Theorem in Isabelle/HOL
Angeliki Koutsoukou Argyraki
,
Mantas Baksys
,
Chelsea Edmonds
.
CPP 2023
:
225-238
[doi]
Formalized Class Group Computations and Integral Points on Mordell Elliptic Curves
Anne Baanen
,
Alex J. Best
,
Nirvana Coppola
,
Sander R. Dahmen
.
CPP 2023
:
47-62
[doi]
CompCert: A Journey through the Landscape of Mechanized Semantics for Verified Compilation (Keynote)
Sandrine Blazy
.
CPP 2023
:
1
[doi]
Compositional Pre-processing for Automated Reasoning in Dependent Type Theory
Valentin Blot
,
Denis Cousineau 0003
,
Enzo Crance
,
Louise Dubois de Prisque
,
Chantal Keller
,
Assia Mahboubi
,
Pierre Vial
.
CPP 2023
:
63-77
[doi]
Encoding Dependently-Typed Constructions into Simple Type Theory
Anthony Bordg
,
Adrián Doña Mateo
.
CPP 2023
:
78-89
[doi]
A Formalized Reduction of Keller's Conjecture
Joshua Clune
.
CPP 2023
:
90-101
[doi]
Compiling Higher-Order Specifications to SMT Solvers: How to Deal with Rejection Constructively
Matthew L. Daggitt
,
Robert Atkey
,
Wen Kokke
,
Ekaterina Komendantskaya
,
Luca Arnaboldi
.
CPP 2023
:
102-120
[doi]
Formalizing and Computing Propositional Quantifiers
Hugo Férée
,
Sam van Gool
.
CPP 2023
:
148-158
[doi]
Practical and Sound Equality Tests, Automatically: Deriving eqType Instances for Jasmin's Data Types with Coq-Elpi
Benjamin Grégoire
,
Jean-Christophe Léchenet
,
Enrico Tassi
.
CPP 2023
:
167-181
[doi]
Mechanised Semantics for Gated Static Single Assignment
Yann Herklotz
,
Delphine Demange
,
Sandrine Blazy
.
CPP 2023
:
182-196
[doi]
Improved Assistance for Interactive Proof (Keynote)
Cezary Kaliszyk
.
CPP 2023
:
2
[doi]
A Formalization of the Development Closedness Criterion for Left-Linear Term Rewrite Systems
Christina Kohl
,
Aart Middeldorp
.
CPP 2023
:
197-210
[doi]
A First Complete Algorithm for Real Quantifier Elimination in Isabelle/HOL
Katherine Kosaian
,
Yong Kiam Tan
,
André Platzer
.
CPP 2023
:
211-224
[doi]
Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2023, Boston, MA, USA, January 16-17, 2023
Robbert Krebbers
,
Dmitriy Traytel
,
Brigitte Pientka
,
Steve Zdancewic
, editors,
ACM,
2023.
[doi]
Computing Cohomology Rings in Cubical Agda
Thomas Lamiaux
,
Axel Ljungström
,
Anders Mörtberg
.
CPP 2023
:
239-252
[doi]
Aesop: White-Box Best-First Proof Search for Lean
Jannis Limperg
,
Asta Halkjær From
.
CPP 2023
:
253-266
[doi]
Formalising Sharkovsky's Theorem (Proof Pearl)
Bhavik Mehta
.
CPP 2023
:
267-274
[doi]
ASN1*: Provably Correct, Non-malleable Parsing for ASN.1 DER
Haobin Ni
,
Antoine Delignat-Lavaud
,
Cédric Fournet
,
Tahina Ramananandro
,
Nikhil Swamy
.
CPP 2023
:
275-289
[doi]
Formalising Decentralised Exchanges in Coq
Eske Hoy Nielsen
,
Danil Annenkov
,
Bas Spitters
.
CPP 2023
:
290-302
[doi]
P4Cub: A Little Language for Big Routers
Rudy Peterson
,
Eric Hayden Campbell
,
John Chen
,
Natalie Isak
,
Calvin Shyu
,
Ryan Doenges
,
Parisa Ataei
,
Nate Foster
.
CPP 2023
:
303-319
[doi]
Formalising the h-Principle and Sphere Eversion
Floris van Doorn
,
Patrick Massot
,
Oliver Nash
.
CPP 2023
:
121-134
[doi]
Verifying Term Graph Optimizations using Isabelle/HOL
Brae J. Webb
,
Ian J. Hayes
,
Mark Utting
.
CPP 2023
:
320-333
[doi]
A Formalization of Doob's Martingale Convergence Theorems in mathlib
Kexing Ying
,
Rémy Degenne
.
CPP 2023
:
334-347
[doi]
2022
CPP '22: 11th ACM SIGPLAN International Conference on Certified Programs and Proofs, Philadelphia, PA, USA, January 17 - 18, 2022
Andrei Popescu 0001
,
Steve Zdancewic
, editors,
ACM,
2022.
[doi]
Implementing a category-theoretic framework for typed abstract syntax
Benedikt Ahrens
,
Ralph Matthes
,
Anders Mörtberg
.
CPP 2022
:
307-323
[doi]
Certified abstract machines for skeletal semantics
Guillaume Ambal
,
Sergueï Lenglet
,
Alan Schmitt
.
CPP 2022
:
55-67
[doi]
The sel4 verification: the art and craft of proof and the reality of commercial support (invited talk)
June Andronick
.
CPP 2022
:
1
[doi]
Coq's vibrant ecosystem for verification engineering (invited talk)
Andrew W. Appel
.
CPP 2022
:
2-11
[doi]
A verified algebraic representation of cairo program execution
Jeremy Avigad
,
Lior Goldberg
,
David Levit
,
Yoav Seginer
,
Alon Titelman
.
CPP 2022
:
153-165
[doi]
Applying formal verification to microkernel IPC at meta
Quentin Carbonneaux
,
Noam Zilberstein
,
Christoph Klee
,
Peter W. O'Hearn
,
Francesco Zappa Nardelli
.
CPP 2022
:
116-129
[doi]
Windmills of the minds: an algorithm for fermat's two squares theorem
Hing-Lun Chan
.
CPP 2022
:
251-264
[doi]
Overcoming restraint: composing verification of foreign functions with cogent
Louis Cheung
,
Liam O'Connor
,
Christine Rizkallah
.
CPP 2022
:
13-26
[doi]
A compositional proof framework for FRETish requirements
Esther Conrad
,
Laura Titolo
,
Dimitra Giannakopoulou
,
Thomas Pressburger
,
Aaron Dutle
.
CPP 2022
:
68-81
[doi]
A drag-and-drop proof tactic
Pablo Donato
,
Pierre-Yves Strub
,
Benjamin Werner
.
CPP 2022
:
197-209
[doi]
Verbatim++: verified, optimized, and semantically rich lexing with derivatives
Derek Egolf
,
Sam Lasser
,
Kathleen Fisher
.
CPP 2022
:
27-39
[doi]
Reflection, rewinding, and coin-toss in EasyCrypt
Denis Firsov
,
Dominique Unruh
.
CPP 2022
:
166-179
[doi]
Semantic cut elimination for the logic of bunched implications, formalized in Coq
Dan Frumin
.
CPP 2022
:
291-306
[doi]
Safe, fast, concurrent proof checking for the lambda-pi calculus modulo rewriting
Michael Färber
.
CPP 2022
:
225-238
[doi]
(Deep) induction rules for GADTs
Patricia Johann
,
Enrico Ghiorzi
.
CPP 2022
:
324-337
[doi]
CertiStr: a certified string solver
Shuanglong Kan
,
Anthony Widjaja Lin
,
Philipp Rümmer
,
Micha Schrader
.
CPP 2022
:
210-224
[doi]
A machine-checked direct proof of the Steiner-lehmus theorem
Ariel Kellison
.
CPP 2022
:
265-273
[doi]
Undecidability, incompleteness, and completeness of second-order logic in Coq
Mark Koch
,
Dominik Kirst
.
CPP 2022
:
274-290
[doi]
An extension of the framework types-to-sets for Isabelle/HOL
Mihails Milehins
.
CPP 2022
:
180-196
[doi]
Specification and verification of a transient stack
Alexandre Moine
,
Arthur Charguéraud
,
François Pottier
.
CPP 2022
:
82-99
[doi]
Structural embeddings revisited (invited talk)
César Muñoz
.
CPP 2022
:
12
[doi]
Formalising lie algebras
Oliver Nash
.
CPP 2022
:
239-250
[doi]
On homotopy of walks and spherical maps in homotopy type theory
Jonathan Prieto-Cubides
.
CPP 2022
:
338-351
[doi]
Formal verification of a distributed dynamic reconfiguration protocol
William Schultz
,
Ian Dardik
,
Stavros Tripakis
.
CPP 2022
:
143-152
[doi]
Formally verified superblock scheduling
Cyril Six
,
Léo Gourdin
,
Sylvain Boulmé
,
David Monniaux
,
Justus Fasse
,
Nicolas Nardino
.
CPP 2022
:
40-54
[doi]
Forward build systems, formally
Sarah Spall
,
Neil Mitchell
,
Sam Tobin-Hochstadt
.
CPP 2022
:
130-142
[doi]
Mechanized verification of a fine-grained concurrent queue from meta's folly library
Simon Friis Vindum
,
Dan Frumin
,
Lars Birkedal
.
CPP 2022
:
100-115
[doi]
2021
Extracting smart contracts tested and verified in Coq
Danil Annenkov
,
Mikkel Milo
,
Jakob Botsch Nielsen
,
Bas Spitters
.
CPP 2021
:
105-121
[doi]
A Coq formalization of data provenance
Véronique Benzaken
,
Sarah Cohen Boulakia
,
Evelyne Contejean
,
Chantal Keller
,
Rébecca Zucchini
.
CPP 2021
:
152-162
[doi]
Developing and certifying Datalog optimizations in coq/mathcomp
Pierre-Léo Bégay
,
Pierre Crégut
,
Jean-François Monin
.
CPP 2021
:
163-177
[doi]
On the formalisation of Kolmogorov complexity
Elliot Catt
,
Michael Norrish
.
CPP 2021
:
291-299
[doi]
Formalizing the ring of Witt vectors
Johan Commelin
,
Robert Y. Lewis
.
CPP 2021
:
264-277
[doi]
An Isabelle/HOL formalization of AProVE's termination method for LLVM IR
Max W. Haslbeck
,
René Thiemann
.
CPP 2021
:
238-249
[doi]
Machine-checked semantic session typing
Jonas Kastberg Hinrichsen
,
Daniël Louwrink
,
Robbert Krebbers
,
Jesper Bengtson
.
CPP 2021
:
178-198
[doi]
CPP '21: 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, Virtual Event, Denmark, January 17-19, 2021
Catalin Hritcu
,
Andrei Popescu 0001
, editors,
ACM,
2021.
[doi]
Formalizing category theory in Agda
Jason Z. S. Hu
,
Jacques Carette
.
CPP 2021
:
327-342
[doi]
An anti-locally-nameless approach to formalizing quantifiers
Olivier Laurent
.
CPP 2021
:
300-312
[doi]
A novice-friendly induction tactic for lean
Jannis Limperg
.
CPP 2021
:
199-211
[doi]
A verified decision procedure for the first-order theory of rewriting for linear variable-separated rewrite systems
Alexander Lochmann
,
Aart Middeldorp
,
Fabian Mitterwallner
,
Bertram Felgenhauer
.
CPP 2021
:
250-263
[doi]
Lutsig: a verified Verilog compiler for verified circuit development
Andreas Lööw
.
CPP 2021
:
46-60
[doi]
Formal verification of authenticated, append-only skip lists in Agda
Victor Cacciari Miraldo
,
Harold Carr
,
Mark Moir
,
Lisandra Silva
,
Guy L. Steele Jr.
.
CPP 2021
:
122-136
[doi]
A minimalistic verified bootstrapped compiler (proof pearl)
Magnus O. Myreen
.
CPP 2021
:
32-45
[doi]
Teaching algorithms and data structures with a proof assistant (invited talk)
Tobias Nipkow
.
CPP 2021
:
1-3
[doi]
Formal verification of semi-algebraic sets and real analytic functions
J. Tanner Slagel
,
Lauren White
,
Aaron Dutle
.
CPP 2021
:
278-290
[doi]
A formal proof of PAC learnability for decision stumps
Joseph Tassarotti
,
Koundinya Vajjha
,
Anindya Banerjee 0001
,
Jean-Baptiste Tristan
.
CPP 2021
:
5-17
[doi]
Reasoning about monotonicity in separation logic
Amin Timany
,
Lars Birkedal
.
CPP 2021
:
91-104
[doi]
A modular Isabelle framework for verifying saturation provers
Sophie Tourret
,
Jasmin Blanchette
.
CPP 2021
:
224-237
[doi]
CertRL: formalizing convergence proofs for value and policy iteration in Coq
Koundinya Vajjha
,
Avraham Shinnar
,
Barry M. Trager
,
Vasily Pestun
,
Nathan Fulton
.
CPP 2021
:
18-31
[doi]
Contextual refinement of the Michael-Scott queue (proof pearl)
Simon Friis Vindum
,
Lars Birkedal
.
CPP 2021
:
76-90
[doi]
Sign in
or
sign up
to see more results.