Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs - CPP 2018
Latest Publications

TOTAL DOCUMENTS

48

(FIVE YEARS 0)

H-INDEX

6

(FIVE YEARS 0)

Published By ACM Press

9781450355865

Latest Documents Most Cited Documents Contributed Authors Related Sources Related Keywords

Efficient certification of complexity proofs: formalizing the Perron–Frobenius theorem (invited talk paper)

Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs - CPP 2018 ◽

10.1145/3167103 ◽

2018 ◽

Cited By ~ 1

Author(s):

Jose Divasón ◽

Sebastiaan Joosten ◽

Ondřej Kunčar ◽

René Thiemann ◽

Akihisa Yamada

Keyword(s):

Frobenius Theorem

Download Full-text

Finite sets in homotopy type theory

Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs - CPP 2018 ◽

10.1145/3167085 ◽

2018 ◽

Cited By ~ 3

Author(s):

Dan Frumin ◽

Herman Geuvers ◽

Léon Gondelman ◽

Niels van der Weide

Keyword(s):

Homotopy Type ◽

Type Theory ◽

Finite Sets ◽

Homotopy Type Theory

Download Full-text

Œuf: minimizing the Coq extraction TCB

Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs - CPP 2018 ◽

10.1145/3167089 ◽

2018 ◽

Cited By ~ 6

Author(s):

Eric Mullen ◽

Stuart Pernsteiner ◽

James R. Wilcox ◽

Zachary Tatlock ◽

Dan Grossman

Download Full-text

Binder aware recursion over well-scoped de Bruijn syntax

Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs - CPP 2018 ◽

10.1145/3167098 ◽

2018 ◽

Cited By ~ 1

Author(s):

Jonas Kaiser ◽

Steven Schäfer ◽

Kathrin Stark

Keyword(s):

De Bruijn

Download Full-text

A two-level logic perspective on (simultaneous) substitutions

Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs - CPP 2018 ◽

10.1145/3167093 ◽

2018 ◽

Author(s):

Kaustuv Chaudhuri

Download Full-text

Mechanising and verifying the WebAssembly specification

Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs - CPP 2018 ◽

10.1145/3167082 ◽

2018 ◽

Cited By ~ 7

Author(s):

Conrad Watt

Download Full-text

Completeness and decidability of converse PDL in the constructive type theory of Coq

Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs - CPP 2018 ◽

10.1145/3167088 ◽

2018 ◽

Author(s):

Christian Doczkal ◽

Joachim Bard

Keyword(s):

Type Theory ◽

Constructive Type Theory ◽

Constructive Type

Download Full-text

Adapting proof automation to adapt proofs

Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs - CPP 2018 ◽

10.1145/3167094 ◽

2018 ◽

Cited By ~ 3

Author(s):

Talia Ringer ◽

Nathaniel Yazdani ◽

John Leo ◽

Dan Grossman

Keyword(s):

Proof Automation

Download Full-text

A constructive formalisation of Semi-algebraic sets and functions

Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs - CPP 2018 ◽

10.1145/3167099 ◽

2018 ◽

Author(s):

Boris Djalal

Keyword(s):

Algebraic Sets

Download Full-text

Generic derivation of induction for impredicative encodings in Cedille

Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs - CPP 2018 ◽

10.1145/3167087 ◽

2018 ◽

Cited By ~ 5

Author(s):

Denis Firsov ◽

Aaron Stump

Download Full-text