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

TOTAL DOCUMENTS

(FIVE YEARS 29)

H-INDEX

(FIVE YEARS 3)

Published By ACM

9781450370974

Latest Documents Most Cited Documents Contributed Authors Related Sources Related Keywords

A functional proof pearl: inverting the Ackermann hierarchy

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

10.1145/3372885.3373837 ◽

2020 ◽

Author(s):

Linh Tran ◽

Anshuman Mohan ◽

Aquinas Hobor

Download Full-text

A formal proof of the independence of the continuum hypothesis

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

10.1145/3372885.3373826 ◽

2020 ◽

Cited By ~ 2

Author(s):

Jesse Michael Han ◽

Floris van Doorn

Keyword(s):

Continuum Hypothesis ◽

Formal Proof ◽

The Continuum

Download Full-text

Frying the egg, roasting the chicken: unit deletions in DRAT proofs

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

10.1145/3372885.3373821 ◽

2020 ◽

Author(s):

Johannes Altmanninger ◽

Adrián Rebola Pardo

Download Full-text

Proof assistants at the hardware-software interface (invited talk)

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

10.1145/3372885.3378575 ◽

2020 ◽

Author(s):

Adam Chlipala

Keyword(s):

Proof Assistants ◽

Software Interface

Download Full-text

Completeness of an axiomatization of graph isomorphism via graph rewriting in Coq

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

10.1145/3372885.3373831 ◽

2020 ◽

Cited By ~ 1

Author(s):

Christian Doczkal ◽

Damien Pous

Keyword(s):

Graph Isomorphism ◽

Graph Rewriting

Download Full-text

ConCert: a smart contract certification framework in Coq

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

10.1145/3372885.3373829 ◽

2020 ◽

Cited By ~ 3

Author(s):

Danil Annenkov ◽

Jakob Botsch Nielsen ◽

Bas Spitters

Keyword(s):

Smart Contract

Download Full-text

Undecidability of higher-order unification formalised in Coq

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

10.1145/3372885.3373832 ◽

2020 ◽

Cited By ~ 1

Author(s):

Simon Spies ◽

Yannick Forster

Keyword(s):

Higher Order

Download Full-text

A mechanized formalization of GraphQL

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

10.1145/3372885.3373822 ◽

2020 ◽

Author(s):

Tomás Díaz ◽

Federico Olmedo ◽

Éric Tanter

Download Full-text

Exploration of neural machine translation in autoformalization of mathematics in Mizar

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

10.1145/3372885.3373827 ◽

2020 ◽

Cited By ~ 1

Author(s):

Qingxiang Wang ◽

Chad Brown ◽

Cezary Kaliszyk ◽

Josef Urban

Keyword(s):

Machine Translation ◽

Neural Machine Translation

Download Full-text

FreeSpec: specifying, verifying, and executing impure computations in Coq

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

10.1145/3372885.3373812 ◽

2020 ◽

Author(s):

Thomas Letan ◽

Yann Régis-Gianas

Download Full-text

Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and ProofsLatest Publications

TOTAL DOCUMENTS

H-INDEX

Published By ACM

A functional proof pearl: inverting the Ackermann hierarchy

A formal proof of the independence of the continuum hypothesis

Frying the egg, roasting the chicken: unit deletions in DRAT proofs

Proof assistants at the hardware-software interface (invited talk)

Completeness of an axiomatization of graph isomorphism via graph rewriting in Coq

ConCert: a smart contract certification framework in Coq

Undecidability of higher-order unification formalised in Coq

A mechanized formalization of GraphQL

Exploration of neural machine translation in autoformalization of mathematics in Mizar

FreeSpec: specifying, verifying, and executing impure computations in Coq

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