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

TOTAL DOCUMENTS

(FIVE YEARS 0)

H-INDEX

(FIVE YEARS 0)

Published By ACM Press

9781450362221

Latest Documents Most Cited Documents Contributed Authors Related Sources Related Keywords

Autosubst 2: reasoning with multi-sorted de Bruijn terms and vector substitutions

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

10.1145/3293880.3294101 ◽

2019 ◽

Cited By ~ 4

Author(s):

Kathrin Stark ◽

Steven Schäfer ◽

Jonas Kaiser

Keyword(s):

De Bruijn

Download Full-text

A linear logical framework in Hybrid (invited talk)

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

10.1145/3293880.3294088 ◽

2019 ◽

Author(s):

Amy P. Felty

Keyword(s):

Logical Framework

Download Full-text

Dynamic class initialization semantics: a Jinja extension

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

10.1145/3293880.3294104 ◽

2019 ◽

Author(s):

Susannah Mansky ◽

Elsa L. Gunter

Download Full-text

Verified solving and asymptotics of linear recurrences

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

10.1145/3293880.3294090 ◽

2019 ◽

Author(s):

Manuel Eberl

Keyword(s):

Linear Recurrences

Download Full-text

Counting polynomial roots in Isabelle/HOL: a formal proof of the Budan-Fourier theorem

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

10.1145/3293880.3294092 ◽

2019 ◽

Author(s):

Wenda Li ◽

Lawrence C. Paulson

Keyword(s):

Formal Proof ◽

Polynomial Roots ◽

Counting Polynomial

Download Full-text

Formal verification of a program obfuscation based on mixed Boolean-arithmetic expressions

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

10.1145/3293880.3294103 ◽

2019 ◽

Cited By ~ 1

Author(s):

Sandrine Blazy ◽

Rémi Hutin

Keyword(s):

Formal Verification ◽

Program Obfuscation ◽

Arithmetic Expressions

Download Full-text

From C to interaction trees: specifying, verifying, and testing a networked server

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

10.1145/3293880.3294106 ◽

2019 ◽

Cited By ~ 9

Author(s):

Nicolas Koh ◽

Yao Li ◽

Yishuai Li ◽

Li-yao Xia ◽

Lennart Beringer ◽

...

Download Full-text

Certified ACKBO

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

10.1145/3293880.3294099 ◽

2019 ◽

Author(s):

Alexander Lochmann ◽

Christian Sternagel

Download Full-text

Certified undecidability of intuitionistic linear logic via binary stack machines and Minsky machines

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

10.1145/3293880.3294096 ◽

2019 ◽

Cited By ~ 4

Author(s):

Yannick Forster ◽

Dominique Larchey-Wendling

Keyword(s):

Linear Logic ◽

Intuitionistic Linear Logic

Download Full-text

A verified prover based on ordered resolution

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

10.1145/3293880.3294100 ◽

2019 ◽

Cited By ~ 4

Author(s):

Anders Schlichtkrull ◽

Jasmin Christian Blanchette ◽

Dmitriy Traytel

Download Full-text

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

TOTAL DOCUMENTS

H-INDEX

Published By ACM Press

Autosubst 2: reasoning with multi-sorted de Bruijn terms and vector substitutions

A linear logical framework in Hybrid (invited talk)

Dynamic class initialization semantics: a Jinja extension

Verified solving and asymptotics of linear recurrences

Counting polynomial roots in Isabelle/HOL: a formal proof of the Budan-Fourier theorem

Formal verification of a program obfuscation based on mixed Boolean-arithmetic expressions

From C to interaction trees: specifying, verifying, and testing a networked server

Certified ACKBO

Certified undecidability of intuitionistic linear logic via binary stack machines and Minsky machines

A verified prover based on ordered resolution

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