Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs
Latest Publications

TOTAL DOCUMENTS

26

(FIVE YEARS 26)

H-INDEX

1

(FIVE YEARS 1)

Published By ACM

9781450382991

Latest Documents Most Cited Documents Contributed Authors Related Sources Related Keywords

The generalised continuum hypothesis implies the axiom of choice in Coq

Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs ◽

10.1145/3437992.3439932 ◽

2021 ◽

Author(s):

Dominik Kirst ◽

Felix Rech

Keyword(s):

Continuum Hypothesis ◽

Axiom Of Choice ◽

The Axiom Of Choice

Download Full-text

Lassie: HOL4 tactics by example

Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs ◽

10.1145/3437992.3439925 ◽

2021 ◽

Author(s):

Heiko Becker ◽

Nathaniel Bos ◽

Ivan Gavran ◽

Eva Darulova ◽

Rupak Majumdar

Download Full-text

Formal verification of authenticated, append-only skip lists in Agda

Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs ◽

10.1145/3437992.3439924 ◽

2021 ◽

Author(s):

Victor Cacciari Miraldo ◽

Harold Carr ◽

Mark Moir ◽

Lisandra Silva ◽

Guy L. Steele Jr.

Keyword(s):

Formal Verification

Download Full-text

On the formalisation of Kolmogorov complexity

Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs ◽

10.1145/3437992.3439921 ◽

2021 ◽

Author(s):

Elliot Catt ◽

Michael Norrish

Keyword(s):

Kolmogorov Complexity

Download Full-text

CertRL: formalizing convergence proofs for value and policy iteration in Coq

Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs ◽

10.1145/3437992.3439927 ◽

2021 ◽

Author(s):

Koundinya Vajjha ◽

Avraham Shinnar ◽

Barry Trager ◽

Vasily Pestun ◽

Nathan Fulton

Keyword(s):

Policy Iteration ◽

Convergence Proofs

Download Full-text

A verified decision procedure for the first-order theory of rewriting for linear variable-separated rewrite systems

Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs ◽

10.1145/3437992.3439918 ◽

2021 ◽

Author(s):

Alexander Lochmann ◽

Aart Middeldorp ◽

Fabian Mitterwallner ◽

Bertram Felgenhauer

Keyword(s):

Decision Procedure ◽

Order Theory ◽

Rewrite Systems ◽

First Order ◽

First Order Theory

Download Full-text

An anti-locally-nameless approach to formalizing quantifiers

Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs ◽

10.1145/3437992.3439926 ◽

2021 ◽

Author(s):

Olivier Laurent

Download Full-text

A novice-friendly induction tactic for lean

Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs ◽

10.1145/3437992.3439928 ◽

2021 ◽

Author(s):

Jannis Limperg

Download Full-text

A minimalistic verified bootstrapped compiler (proof pearl)

Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs ◽

10.1145/3437992.3439915 ◽

2021 ◽

Author(s):

Magnus O. Myreen

Download Full-text

An Isabelle/HOL formalization of AProVE’s termination method for LLVM IR

Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs ◽

10.1145/3437992.3439935 ◽

2021 ◽

Author(s):

Max W. Haslbeck ◽

René Thiemann

Download Full-text