| |
Benzaken, Véronique
|
CPP '19: "A Coq Mechanised Formal Semantics ..."
A Coq Mechanised Formal Semantics for Realistic SQL Queries: Formally Reconciling SQL and Bag Relational Algebra
Véronique Benzaken and Évelyne Contejean
(University of Paris-Sud, France; LRI, France; CNRS, France)
@InProceedings{CPP19p326,
author = {Véronique Benzaken and Évelyne Contejean},
title = {A Coq Mechanised Formal Semantics for Realistic SQL Queries: Formally Reconciling SQL and Bag Relational Algebra},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {326-325},
doi = {10.1145/3293880.3294107},
year = {2019},
}
 Publisher's Version
Article: poplws19cppmain-id1-p doi:10.1145/3293880.3294107
|
| |
Beringer, Lennart |
CPP '19: "From C to Interaction Trees: ..."
From C to Interaction Trees: Specifying, Verifying, and Testing a Networked Server
Nicolas Koh, Yao Li, Yishuai Li, Li-yao Xia, Lennart Beringer, Wolf Honoré, William Mansky, Benjamin C. Pierce, and Steve Zdancewic
(University of Pennsylvania, USA; Princeton University, USA; Yale University, USA; University of Illinois at Chicago, USA)
@InProceedings{CPP19p309,
author = {Nicolas Koh and Yao Li and Yishuai Li and Li-yao Xia and Lennart Beringer and Wolf Honoré and William Mansky and Benjamin C. Pierce and Steve Zdancewic},
title = {From C to Interaction Trees: Specifying, Verifying, and Testing a Networked Server},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {309-308},
doi = {10.1145/3293880.3294106},
year = {2019},
}
Publisher's Version
Article: poplws19cppmain-id22-p doi:10.1145/3293880.3294106
|
| |
Blanchette, Jasmin Christian |
CPP '19: "Formalizing the Metatheory ..."
Formalizing the Metatheory of Logical Calculi and Automatic Provers in Isabelle/HOL (Invited Talk)
Jasmin Christian Blanchette
(Vrije Universiteit Amsterdam, Netherlands)
@InProceedings{CPP19p1,
author = {Jasmin Christian Blanchette},
title = {Formalizing the Metatheory of Logical Calculi and Automatic Provers in Isabelle/HOL (Invited Talk)},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {1-0},
doi = {10.1145/3293880.3294087},
year = {2019},
}
Publisher's Version
Article: poplws19cppmain-id100-p doi:10.1145/3293880.3294087
CPP '19: "A Verified Prover Based on ..."
A Verified Prover Based on Ordered Resolution
Anders Schlichtkrull, Jasmin Christian Blanchette, and Dmitriy Traytel
(DTU, Denmark; Vrije Universiteit Amsterdam, Netherlands; ETH Zurich, Switzerland)
@InProceedings{CPP19p207,
author = {Anders Schlichtkrull and Jasmin Christian Blanchette and Dmitriy Traytel},
title = {A Verified Prover Based on Ordered Resolution},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {207-206},
doi = {10.1145/3293880.3294100},
year = {2019},
}
Publisher's Version
Article: poplws19cppmain-id7-p doi:10.1145/3293880.3294100
|
| |
Blazy, Sandrine |
CPP '19: "Formal Verification of a Program ..."
Formal Verification of a Program Obfuscation Based on Mixed Boolean-Arithmetic Expressions
Sandrine Blazy and Rémi Hutin
(University of Rennes, France; Inria, France; CNRS, France; IRISA, France)
@InProceedings{CPP19p258,
author = {Sandrine Blazy and Rémi Hutin},
title = {Formal Verification of a Program Obfuscation Based on Mixed Boolean-Arithmetic Expressions},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {258-257},
doi = {10.1145/3293880.3294103},
year = {2019},
}
Publisher's Version
Article: poplws19cppmain-id9-p doi:10.1145/3293880.3294103
|
| |
Chaudhuri, Kaustuv
|
CPP '19: "A Proof-Theoretic Approach ..."
A Proof-Theoretic Approach to Certifying Skolemization
Kaustuv Chaudhuri, Matteo Manighetti, and Dale Miller
(Inria, France; LIX, France; École Polytechnique, France)
@InProceedings{CPP19p105,
author = {Kaustuv Chaudhuri and Matteo Manighetti and Dale Miller},
title = {A Proof-Theoretic Approach to Certifying Skolemization},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {105-104},
doi = {10.1145/3293880.3294094},
year = {2019},
}
Publisher's Version
Article: poplws19cppmain-id24-p doi:10.1145/3293880.3294094
|
| |
Contejean, Évelyne |
CPP '19: "A Coq Mechanised Formal Semantics ..."
A Coq Mechanised Formal Semantics for Realistic SQL Queries: Formally Reconciling SQL and Bag Relational Algebra
Véronique Benzaken and Évelyne Contejean
(University of Paris-Sud, France; LRI, France; CNRS, France)
@InProceedings{CPP19p326,
author = {Véronique Benzaken and Évelyne Contejean},
title = {A Coq Mechanised Formal Semantics for Realistic SQL Queries: Formally Reconciling SQL and Bag Relational Algebra},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {326-325},
doi = {10.1145/3293880.3294107},
year = {2019},
}
Publisher's Version
Article: poplws19cppmain-id1-p doi:10.1145/3293880.3294107
|
| |
Delaware, Benjamin
|
CPP '19: "A Verified Protocol Buffer ..."
A Verified Protocol Buffer Compiler
Qianchuan Ye and Benjamin Delaware
(Purdue University, USA)
@InProceedings{CPP19p292,
author = {Qianchuan Ye and Benjamin Delaware},
title = {A Verified Protocol Buffer Compiler},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {292-291},
doi = {10.1145/3293880.3294105},
year = {2019},
}
Publisher's Version
 Published Artifact
Artifacts Available
Article: poplws19cppmain-id21-p doi:10.1145/3293880.3294105
|
| |
Eberl, Manuel
|
CPP '19: "Verified Solving and Asymptotics ..."
Verified Solving and Asymptotics of Linear Recurrences
Manuel Eberl
(TU Munich, Germany)
@InProceedings{CPP19p37,
author = {Manuel Eberl},
title = {Verified Solving and Asymptotics of Linear Recurrences},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {37-36},
doi = {10.1145/3293880.3294090},
year = {2019},
}
Publisher's Version
Article: poplws19cppmain-id5-p doi:10.1145/3293880.3294090
|
| |
Felgenhauer, Bertram
|
CPP '19: "A Verified Ground Confluence ..."
A Verified Ground Confluence Tool for Linear Variable-Separated Rewrite Systems in Isabelle/HOL
Bertram Felgenhauer, Aart Middeldorp, T. V. H. Prathamesh, and Franziska Rapp
(University of Innsbruck, Austria; Allgemeines Rechenzentrum Innsbruck, Austria)
@InProceedings{CPP19p173,
author = {Bertram Felgenhauer and Aart Middeldorp and T. V. H. Prathamesh and Franziska Rapp},
title = {A Verified Ground Confluence Tool for Linear Variable-Separated Rewrite Systems in Isabelle/HOL},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {173-172},
doi = {10.1145/3293880.3294098},
year = {2019},
}
Publisher's Version
Article: poplws19cppmain-id18-p doi:10.1145/3293880.3294098
|
| |
Felty, Amy P. |
CPP '19: "A Linear Logical Framework ..."
A Linear Logical Framework in Hybrid (Invited Talk)
Amy P. Felty
(University of Ottawa, Canada)
@InProceedings{CPP19p18,
author = {Amy P. Felty},
title = {A Linear Logical Framework in Hybrid (Invited Talk)},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {18-17},
doi = {10.1145/3293880.3294088},
year = {2019},
}
Publisher's Version
Article: poplws19cppmain-id101-p doi:10.1145/3293880.3294088
|
| |
Forster, Yannick |
CPP '19: "Certified Undecidability of ..."
Certified Undecidability of Intuitionistic Linear Logic via Binary Stack Machines and Minsky Machines
Yannick Forster and Dominique Larchey-Wendling
(Saarland University, Germany; University of Lorraine, France; CNRS, France; LORIA, France)
@InProceedings{CPP19p139,
author = {Yannick Forster and Dominique Larchey-Wendling},
title = {Certified Undecidability of Intuitionistic Linear Logic via Binary Stack Machines and Minsky Machines},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {139-138},
doi = {10.1145/3293880.3294096},
year = {2019},
}
Publisher's Version
Article: poplws19cppmain-id27-p doi:10.1145/3293880.3294096
CPP '19: "Call-By-Push-Value in Coq: ..."
Call-By-Push-Value in Coq: Operational, Equational, and Denotational Theory
Yannick Forster, Steven Schäfer, Simon Spies, and Kathrin Stark
(Saarland University, Germany)
@InProceedings{CPP19p156,
author = {Yannick Forster and Steven Schäfer and Simon Spies and Kathrin Stark},
title = {Call-By-Push-Value in Coq: Operational, Equational, and Denotational Theory},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {156-155},
doi = {10.1145/3293880.3294097},
year = {2019},
}
Publisher's Version
Article: poplws19cppmain-id43-p doi:10.1145/3293880.3294097
CPP '19: "On Synthetic Undecidability ..."
On Synthetic Undecidability in Coq, with an Application to the Entscheidungsproblem
Yannick Forster, Dominik Kirst, and Gert Smolka
(Saarland University, Germany)
@InProceedings{CPP19p54,
author = {Yannick Forster and Dominik Kirst and Gert Smolka},
title = {On Synthetic Undecidability in Coq, with an Application to the Entscheidungsproblem},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {54-53},
doi = {10.1145/3293880.3294091},
year = {2019},
}
Publisher's Version
Article: poplws19cppmain-id38-p doi:10.1145/3293880.3294091
|
| |
Gunter, Elsa L.
|
CPP '19: "Dynamic Class Initialization ..."
Dynamic Class Initialization Semantics: A Jinja Extension
Susannah Mansky and Elsa L. Gunter
(University of Illinois at Urbana-Champaign, USA)
@InProceedings{CPP19p275,
author = {Susannah Mansky and Elsa L. Gunter},
title = {Dynamic Class Initialization Semantics: A Jinja Extension},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {275-274},
doi = {10.1145/3293880.3294104},
year = {2019},
}
Publisher's Version
Article: poplws19cppmain-id40-p doi:10.1145/3293880.3294104
|
| |
Honoré, Wolf
|
CPP '19: "From C to Interaction Trees: ..."
From C to Interaction Trees: Specifying, Verifying, and Testing a Networked Server
Nicolas Koh, Yao Li, Yishuai Li, Li-yao Xia, Lennart Beringer, Wolf Honoré, William Mansky, Benjamin C. Pierce, and Steve Zdancewic
(University of Pennsylvania, USA; Princeton University, USA; Yale University, USA; University of Illinois at Chicago, USA)
@InProceedings{CPP19p309,
author = {Nicolas Koh and Yao Li and Yishuai Li and Li-yao Xia and Lennart Beringer and Wolf Honoré and William Mansky and Benjamin C. Pierce and Steve Zdancewic},
title = {From C to Interaction Trees: Specifying, Verifying, and Testing a Networked Server},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {309-308},
doi = {10.1145/3293880.3294106},
year = {2019},
}
Publisher's Version
Article: poplws19cppmain-id22-p doi:10.1145/3293880.3294106
|
| |
Hutin, Rémi |
CPP '19: "Formal Verification of a Program ..."
Formal Verification of a Program Obfuscation Based on Mixed Boolean-Arithmetic Expressions
Sandrine Blazy and Rémi Hutin
(University of Rennes, France; Inria, France; CNRS, France; IRISA, France)
@InProceedings{CPP19p258,
author = {Sandrine Blazy and Rémi Hutin},
title = {Formal Verification of a Program Obfuscation Based on Mixed Boolean-Arithmetic Expressions},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {258-257},
doi = {10.1145/3293880.3294103},
year = {2019},
}
Publisher's Version
Article: poplws19cppmain-id9-p doi:10.1145/3293880.3294103
|
| |
Immler, Fabian
|
CPP '19: "Smooth Manifolds and Types ..."
Smooth Manifolds and Types to Sets for Linear Algebra in Isabelle/HOL
Fabian Immler and Bohua Zhan
(Carnegie Mellon University, USA; Institute of Software at Chinese Academy of Sciences, China)
@InProceedings{CPP19p88,
author = {Fabian Immler and Bohua Zhan},
title = {Smooth Manifolds and Types to Sets for Linear Algebra in Isabelle/HOL},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {88-87},
doi = {10.1145/3293880.3294093},
year = {2019},
}
Publisher's Version
Article: poplws19cppmain-id10-p doi:10.1145/3293880.3294093
|
| |
Kaiser, Jonas
|
CPP '19: "Autosubst 2: Reasoning with ..."
Autosubst 2: Reasoning with Multi-sorted de Bruijn Terms and Vector Substitutions
Kathrin Stark, Steven Schäfer, and Jonas Kaiser
(Saarland University, Germany)
@InProceedings{CPP19p224,
author = {Kathrin Stark and Steven Schäfer and Jonas Kaiser},
title = {Autosubst 2: Reasoning with Multi-sorted de Bruijn Terms and Vector Substitutions},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {224-223},
doi = {10.1145/3293880.3294101},
year = {2019},
}
Publisher's Version
Article: poplws19cppmain-id44-p doi:10.1145/3293880.3294101
|
| |
Kirst, Dominik |
CPP '19: "On Synthetic Undecidability ..."
On Synthetic Undecidability in Coq, with an Application to the Entscheidungsproblem
Yannick Forster, Dominik Kirst, and Gert Smolka
(Saarland University, Germany)
@InProceedings{CPP19p54,
author = {Yannick Forster and Dominik Kirst and Gert Smolka},
title = {On Synthetic Undecidability in Coq, with an Application to the Entscheidungsproblem},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {54-53},
doi = {10.1145/3293880.3294091},
year = {2019},
}
Publisher's Version
Article: poplws19cppmain-id38-p doi:10.1145/3293880.3294091
|
| |
Koh, Nicolas |
CPP '19: "From C to Interaction Trees: ..."
From C to Interaction Trees: Specifying, Verifying, and Testing a Networked Server
Nicolas Koh, Yao Li, Yishuai Li, Li-yao Xia, Lennart Beringer, Wolf Honoré, William Mansky, Benjamin C. Pierce, and Steve Zdancewic
(University of Pennsylvania, USA; Princeton University, USA; Yale University, USA; University of Illinois at Chicago, USA)
@InProceedings{CPP19p309,
author = {Nicolas Koh and Yao Li and Yishuai Li and Li-yao Xia and Lennart Beringer and Wolf Honoré and William Mansky and Benjamin C. Pierce and Steve Zdancewic},
title = {From C to Interaction Trees: Specifying, Verifying, and Testing a Networked Server},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {309-308},
doi = {10.1145/3293880.3294106},
year = {2019},
}
Publisher's Version
Article: poplws19cppmain-id22-p doi:10.1145/3293880.3294106
|
| |
Larchey-Wendling, Dominique
|
CPP '19: "Certified Undecidability of ..."
Certified Undecidability of Intuitionistic Linear Logic via Binary Stack Machines and Minsky Machines
Yannick Forster and Dominique Larchey-Wendling
(Saarland University, Germany; University of Lorraine, France; CNRS, France; LORIA, France)
@InProceedings{CPP19p139,
author = {Yannick Forster and Dominique Larchey-Wendling},
title = {Certified Undecidability of Intuitionistic Linear Logic via Binary Stack Machines and Minsky Machines},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {139-138},
doi = {10.1145/3293880.3294096},
year = {2019},
}
Publisher's Version
Article: poplws19cppmain-id27-p doi:10.1145/3293880.3294096
|
| |
Lewis, Robert Y. |
CPP '19: "A Formal Proof of Hensel's ..."
A Formal Proof of Hensel's Lemma over the p-adic Integers
Robert Y. Lewis
(Vrije Universiteit Amsterdam, Netherlands)
@InProceedings{CPP19p20,
author = {Robert Y. Lewis},
title = {A Formal Proof of Hensel's Lemma over the p-adic Integers},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {20-19},
doi = {10.1145/3293880.3294089},
year = {2019},
}
Publisher's Version
Article: poplws19cppmain-id4-p doi:10.1145/3293880.3294089
|
| |
Li, Wenda |
CPP '19: "Counting Polynomial Roots ..."
Counting Polynomial Roots in Isabelle/HOL: A Formal Proof of the Budan-Fourier Theorem
Wenda Li and Lawrence C. Paulson
(University of Cambridge, UK)
@InProceedings{CPP19p71,
author = {Wenda Li and Lawrence C. Paulson},
title = {Counting Polynomial Roots in Isabelle/HOL: A Formal Proof of the Budan-Fourier Theorem},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {71-70},
doi = {10.1145/3293880.3294092},
year = {2019},
}
Publisher's Version
Article: poplws19cppmain-id31-p doi:10.1145/3293880.3294092
|
| |
Li, Yao |
CPP '19: "From C to Interaction Trees: ..."
From C to Interaction Trees: Specifying, Verifying, and Testing a Networked Server
Nicolas Koh, Yao Li, Yishuai Li, Li-yao Xia, Lennart Beringer, Wolf Honoré, William Mansky, Benjamin C. Pierce, and Steve Zdancewic
(University of Pennsylvania, USA; Princeton University, USA; Yale University, USA; University of Illinois at Chicago, USA)
@InProceedings{CPP19p309,
author = {Nicolas Koh and Yao Li and Yishuai Li and Li-yao Xia and Lennart Beringer and Wolf Honoré and William Mansky and Benjamin C. Pierce and Steve Zdancewic},
title = {From C to Interaction Trees: Specifying, Verifying, and Testing a Networked Server},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {309-308},
doi = {10.1145/3293880.3294106},
year = {2019},
}
Publisher's Version
Article: poplws19cppmain-id22-p doi:10.1145/3293880.3294106
|
| |
Li, Yishuai |
CPP '19: "From C to Interaction Trees: ..."
From C to Interaction Trees: Specifying, Verifying, and Testing a Networked Server
Nicolas Koh, Yao Li, Yishuai Li, Li-yao Xia, Lennart Beringer, Wolf Honoré, William Mansky, Benjamin C. Pierce, and Steve Zdancewic
(University of Pennsylvania, USA; Princeton University, USA; Yale University, USA; University of Illinois at Chicago, USA)
@InProceedings{CPP19p309,
author = {Nicolas Koh and Yao Li and Yishuai Li and Li-yao Xia and Lennart Beringer and Wolf Honoré and William Mansky and Benjamin C. Pierce and Steve Zdancewic},
title = {From C to Interaction Trees: Specifying, Verifying, and Testing a Networked Server},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {309-308},
doi = {10.1145/3293880.3294106},
year = {2019},
}
Publisher's Version
Article: poplws19cppmain-id22-p doi:10.1145/3293880.3294106
|
| |
Lochmann, Alexander |
CPP '19: "Certified ACKBO ..."
Certified ACKBO
Alexander Lochmann and Christian Sternagel
(University of Innsbruck, Austria)
@InProceedings{CPP19p190,
author = {Alexander Lochmann and Christian Sternagel},
title = {Certified ACKBO},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {190-189},
doi = {10.1145/3293880.3294099},
year = {2019},
}
Publisher's Version
Article: poplws19cppmain-id33-p doi:10.1145/3293880.3294099
|
| |
Manighetti, Matteo
|
CPP '19: "A Proof-Theoretic Approach ..."
A Proof-Theoretic Approach to Certifying Skolemization
Kaustuv Chaudhuri, Matteo Manighetti, and Dale Miller
(Inria, France; LIX, France; École Polytechnique, France)
@InProceedings{CPP19p105,
author = {Kaustuv Chaudhuri and Matteo Manighetti and Dale Miller},
title = {A Proof-Theoretic Approach to Certifying Skolemization},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {105-104},
doi = {10.1145/3293880.3294094},
year = {2019},
}
Publisher's Version
Article: poplws19cppmain-id24-p doi:10.1145/3293880.3294094
|
| |
Mansky, Susannah |
CPP '19: "Dynamic Class Initialization ..."
Dynamic Class Initialization Semantics: A Jinja Extension
Susannah Mansky and Elsa L. Gunter
(University of Illinois at Urbana-Champaign, USA)
@InProceedings{CPP19p275,
author = {Susannah Mansky and Elsa L. Gunter},
title = {Dynamic Class Initialization Semantics: A Jinja Extension},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {275-274},
doi = {10.1145/3293880.3294104},
year = {2019},
}
Publisher's Version
Article: poplws19cppmain-id40-p doi:10.1145/3293880.3294104
|
| |
Mansky, William |
CPP '19: "From C to Interaction Trees: ..."
From C to Interaction Trees: Specifying, Verifying, and Testing a Networked Server
Nicolas Koh, Yao Li, Yishuai Li, Li-yao Xia, Lennart Beringer, Wolf Honoré, William Mansky, Benjamin C. Pierce, and Steve Zdancewic
(University of Pennsylvania, USA; Princeton University, USA; Yale University, USA; University of Illinois at Chicago, USA)
@InProceedings{CPP19p309,
author = {Nicolas Koh and Yao Li and Yishuai Li and Li-yao Xia and Lennart Beringer and Wolf Honoré and William Mansky and Benjamin C. Pierce and Steve Zdancewic},
title = {From C to Interaction Trees: Specifying, Verifying, and Testing a Networked Server},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {309-308},
doi = {10.1145/3293880.3294106},
year = {2019},
}
Publisher's Version
Article: poplws19cppmain-id22-p doi:10.1145/3293880.3294106
|
| |
Middeldorp, Aart |
CPP '19: "A Verified Ground Confluence ..."
A Verified Ground Confluence Tool for Linear Variable-Separated Rewrite Systems in Isabelle/HOL
Bertram Felgenhauer, Aart Middeldorp, T. V. H. Prathamesh, and Franziska Rapp
(University of Innsbruck, Austria; Allgemeines Rechenzentrum Innsbruck, Austria)
@InProceedings{CPP19p173,
author = {Bertram Felgenhauer and Aart Middeldorp and T. V. H. Prathamesh and Franziska Rapp},
title = {A Verified Ground Confluence Tool for Linear Variable-Separated Rewrite Systems in Isabelle/HOL},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {173-172},
doi = {10.1145/3293880.3294098},
year = {2019},
}
Publisher's Version
Article: poplws19cppmain-id18-p doi:10.1145/3293880.3294098
|
| |
Miller, Dale |
CPP '19: "A Proof-Theoretic Approach ..."
A Proof-Theoretic Approach to Certifying Skolemization
Kaustuv Chaudhuri, Matteo Manighetti, and Dale Miller
(Inria, France; LIX, France; École Polytechnique, France)
@InProceedings{CPP19p105,
author = {Kaustuv Chaudhuri and Matteo Manighetti and Dale Miller},
title = {A Proof-Theoretic Approach to Certifying Skolemization},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {105-104},
doi = {10.1145/3293880.3294094},
year = {2019},
}
Publisher's Version
Article: poplws19cppmain-id24-p doi:10.1145/3293880.3294094
|
| |
Paulson, Lawrence C.
|
CPP '19: "Counting Polynomial Roots ..."
Counting Polynomial Roots in Isabelle/HOL: A Formal Proof of the Budan-Fourier Theorem
Wenda Li and Lawrence C. Paulson
(University of Cambridge, UK)
@InProceedings{CPP19p71,
author = {Wenda Li and Lawrence C. Paulson},
title = {Counting Polynomial Roots in Isabelle/HOL: A Formal Proof of the Budan-Fourier Theorem},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {71-70},
doi = {10.1145/3293880.3294092},
year = {2019},
}
Publisher's Version
Article: poplws19cppmain-id31-p doi:10.1145/3293880.3294092
|
| |
Pierce, Benjamin C. |
CPP '19: "From C to Interaction Trees: ..."
From C to Interaction Trees: Specifying, Verifying, and Testing a Networked Server
Nicolas Koh, Yao Li, Yishuai Li, Li-yao Xia, Lennart Beringer, Wolf Honoré, William Mansky, Benjamin C. Pierce, and Steve Zdancewic
(University of Pennsylvania, USA; Princeton University, USA; Yale University, USA; University of Illinois at Chicago, USA)
@InProceedings{CPP19p309,
author = {Nicolas Koh and Yao Li and Yishuai Li and Li-yao Xia and Lennart Beringer and Wolf Honoré and William Mansky and Benjamin C. Pierce and Steve Zdancewic},
title = {From C to Interaction Trees: Specifying, Verifying, and Testing a Networked Server},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {309-308},
doi = {10.1145/3293880.3294106},
year = {2019},
}
Publisher's Version
Article: poplws19cppmain-id22-p doi:10.1145/3293880.3294106
|
| |
Prathamesh, T. V. H. |
CPP '19: "A Verified Ground Confluence ..."
A Verified Ground Confluence Tool for Linear Variable-Separated Rewrite Systems in Isabelle/HOL
Bertram Felgenhauer, Aart Middeldorp, T. V. H. Prathamesh, and Franziska Rapp
(University of Innsbruck, Austria; Allgemeines Rechenzentrum Innsbruck, Austria)
@InProceedings{CPP19p173,
author = {Bertram Felgenhauer and Aart Middeldorp and T. V. H. Prathamesh and Franziska Rapp},
title = {A Verified Ground Confluence Tool for Linear Variable-Separated Rewrite Systems in Isabelle/HOL},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {173-172},
doi = {10.1145/3293880.3294098},
year = {2019},
}
Publisher's Version
Article: poplws19cppmain-id18-p doi:10.1145/3293880.3294098
|
| |
Rapp, Franziska
|
CPP '19: "A Verified Ground Confluence ..."
A Verified Ground Confluence Tool for Linear Variable-Separated Rewrite Systems in Isabelle/HOL
Bertram Felgenhauer, Aart Middeldorp, T. V. H. Prathamesh, and Franziska Rapp
(University of Innsbruck, Austria; Allgemeines Rechenzentrum Innsbruck, Austria)
@InProceedings{CPP19p173,
author = {Bertram Felgenhauer and Aart Middeldorp and T. V. H. Prathamesh and Franziska Rapp},
title = {A Verified Ground Confluence Tool for Linear Variable-Separated Rewrite Systems in Isabelle/HOL},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {173-172},
doi = {10.1145/3293880.3294098},
year = {2019},
}
Publisher's Version
Article: poplws19cppmain-id18-p doi:10.1145/3293880.3294098
|
| |
Ravindran, Binoy |
CPP '19: "Formally Verified Big Step ..."
Formally Verified Big Step Semantics out of x86-64 Binaries
Ian Roessle, Freek Verbeek, and Binoy Ravindran
(Virginia Tech, USA)
@InProceedings{CPP19p241,
author = {Ian Roessle and Freek Verbeek and Binoy Ravindran},
title = {Formally Verified Big Step Semantics out of x86-64 Binaries},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {241-240},
doi = {10.1145/3293880.3294102},
year = {2019},
}
Publisher's Version
Article: poplws19cppmain-id20-p doi:10.1145/3293880.3294102
|
| |
Roessle, Ian |
CPP '19: "Formally Verified Big Step ..."
Formally Verified Big Step Semantics out of x86-64 Binaries
Ian Roessle, Freek Verbeek, and Binoy Ravindran
(Virginia Tech, USA)
@InProceedings{CPP19p241,
author = {Ian Roessle and Freek Verbeek and Binoy Ravindran},
title = {Formally Verified Big Step Semantics out of x86-64 Binaries},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {241-240},
doi = {10.1145/3293880.3294102},
year = {2019},
}
Publisher's Version
Article: poplws19cppmain-id20-p doi:10.1145/3293880.3294102
|
| |
Schäfer, Steven
|
CPP '19: "Call-By-Push-Value in Coq: ..."
Call-By-Push-Value in Coq: Operational, Equational, and Denotational Theory
Yannick Forster, Steven Schäfer, Simon Spies, and Kathrin Stark
(Saarland University, Germany)
@InProceedings{CPP19p156,
author = {Yannick Forster and Steven Schäfer and Simon Spies and Kathrin Stark},
title = {Call-By-Push-Value in Coq: Operational, Equational, and Denotational Theory},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {156-155},
doi = {10.1145/3293880.3294097},
year = {2019},
}
Publisher's Version
Article: poplws19cppmain-id43-p doi:10.1145/3293880.3294097
CPP '19: "Autosubst 2: Reasoning with ..."
Autosubst 2: Reasoning with Multi-sorted de Bruijn Terms and Vector Substitutions
Kathrin Stark, Steven Schäfer, and Jonas Kaiser
(Saarland University, Germany)
@InProceedings{CPP19p224,
author = {Kathrin Stark and Steven Schäfer and Jonas Kaiser},
title = {Autosubst 2: Reasoning with Multi-sorted de Bruijn Terms and Vector Substitutions},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {224-223},
doi = {10.1145/3293880.3294101},
year = {2019},
}
Publisher's Version
Article: poplws19cppmain-id44-p doi:10.1145/3293880.3294101
|
| |
Schlichtkrull, Anders |
CPP '19: "A Verified Prover Based on ..."
A Verified Prover Based on Ordered Resolution
Anders Schlichtkrull, Jasmin Christian Blanchette, and Dmitriy Traytel
(DTU, Denmark; Vrije Universiteit Amsterdam, Netherlands; ETH Zurich, Switzerland)
@InProceedings{CPP19p207,
author = {Anders Schlichtkrull and Jasmin Christian Blanchette and Dmitriy Traytel},
title = {A Verified Prover Based on Ordered Resolution},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {207-206},
doi = {10.1145/3293880.3294100},
year = {2019},
}
Publisher's Version
Article: poplws19cppmain-id7-p doi:10.1145/3293880.3294100
|
| |
Smolka, Gert |
CPP '19: "On Synthetic Undecidability ..."
On Synthetic Undecidability in Coq, with an Application to the Entscheidungsproblem
Yannick Forster, Dominik Kirst, and Gert Smolka
(Saarland University, Germany)
@InProceedings{CPP19p54,
author = {Yannick Forster and Dominik Kirst and Gert Smolka},
title = {On Synthetic Undecidability in Coq, with an Application to the Entscheidungsproblem},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {54-53},
doi = {10.1145/3293880.3294091},
year = {2019},
}
Publisher's Version
Article: poplws19cppmain-id38-p doi:10.1145/3293880.3294091
|
| |
Sozeau, Matthieu |
CPP '19: "Eliminating Reflection from ..."
Eliminating Reflection from Type Theory
Théo Winterhalter, Matthieu Sozeau, and Nicolas Tabareau
(Inria, France)
@InProceedings{CPP19p122,
author = {Théo Winterhalter and Matthieu Sozeau and Nicolas Tabareau},
title = {Eliminating Reflection from Type Theory},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {122-121},
doi = {10.1145/3293880.3294095},
year = {2019},
}
Publisher's Version
Article: poplws19cppmain-id30-p doi:10.1145/3293880.3294095
|
| |
Spies, Simon |
CPP '19: "Call-By-Push-Value in Coq: ..."
Call-By-Push-Value in Coq: Operational, Equational, and Denotational Theory
Yannick Forster, Steven Schäfer, Simon Spies, and Kathrin Stark
(Saarland University, Germany)
@InProceedings{CPP19p156,
author = {Yannick Forster and Steven Schäfer and Simon Spies and Kathrin Stark},
title = {Call-By-Push-Value in Coq: Operational, Equational, and Denotational Theory},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {156-155},
doi = {10.1145/3293880.3294097},
year = {2019},
}
Publisher's Version
Article: poplws19cppmain-id43-p doi:10.1145/3293880.3294097
|
| |
Stark, Kathrin |
CPP '19: "Call-By-Push-Value in Coq: ..."
Call-By-Push-Value in Coq: Operational, Equational, and Denotational Theory
Yannick Forster, Steven Schäfer, Simon Spies, and Kathrin Stark
(Saarland University, Germany)
@InProceedings{CPP19p156,
author = {Yannick Forster and Steven Schäfer and Simon Spies and Kathrin Stark},
title = {Call-By-Push-Value in Coq: Operational, Equational, and Denotational Theory},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {156-155},
doi = {10.1145/3293880.3294097},
year = {2019},
}
Publisher's Version
Article: poplws19cppmain-id43-p doi:10.1145/3293880.3294097
CPP '19: "Autosubst 2: Reasoning with ..."
Autosubst 2: Reasoning with Multi-sorted de Bruijn Terms and Vector Substitutions
Kathrin Stark, Steven Schäfer, and Jonas Kaiser
(Saarland University, Germany)
@InProceedings{CPP19p224,
author = {Kathrin Stark and Steven Schäfer and Jonas Kaiser},
title = {Autosubst 2: Reasoning with Multi-sorted de Bruijn Terms and Vector Substitutions},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {224-223},
doi = {10.1145/3293880.3294101},
year = {2019},
}
Publisher's Version
Article: poplws19cppmain-id44-p doi:10.1145/3293880.3294101
|
| |
Sternagel, Christian |
CPP '19: "Certified ACKBO ..."
Certified ACKBO
Alexander Lochmann and Christian Sternagel
(University of Innsbruck, Austria)
@InProceedings{CPP19p190,
author = {Alexander Lochmann and Christian Sternagel},
title = {Certified ACKBO},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {190-189},
doi = {10.1145/3293880.3294099},
year = {2019},
}
Publisher's Version
Article: poplws19cppmain-id33-p doi:10.1145/3293880.3294099
|
| |
Tabareau, Nicolas
|
CPP '19: "Eliminating Reflection from ..."
Eliminating Reflection from Type Theory
Théo Winterhalter, Matthieu Sozeau, and Nicolas Tabareau
(Inria, France)
@InProceedings{CPP19p122,
author = {Théo Winterhalter and Matthieu Sozeau and Nicolas Tabareau},
title = {Eliminating Reflection from Type Theory},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {122-121},
doi = {10.1145/3293880.3294095},
year = {2019},
}
Publisher's Version
Article: poplws19cppmain-id30-p doi:10.1145/3293880.3294095
|
| |
Traytel, Dmitriy |
CPP '19: "A Verified Prover Based on ..."
A Verified Prover Based on Ordered Resolution
Anders Schlichtkrull, Jasmin Christian Blanchette, and Dmitriy Traytel
(DTU, Denmark; Vrije Universiteit Amsterdam, Netherlands; ETH Zurich, Switzerland)
@InProceedings{CPP19p207,
author = {Anders Schlichtkrull and Jasmin Christian Blanchette and Dmitriy Traytel},
title = {A Verified Prover Based on Ordered Resolution},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {207-206},
doi = {10.1145/3293880.3294100},
year = {2019},
}
Publisher's Version
Article: poplws19cppmain-id7-p doi:10.1145/3293880.3294100
|
| |
Verbeek, Freek
|
CPP '19: "Formally Verified Big Step ..."
Formally Verified Big Step Semantics out of x86-64 Binaries
Ian Roessle, Freek Verbeek, and Binoy Ravindran
(Virginia Tech, USA)
@InProceedings{CPP19p241,
author = {Ian Roessle and Freek Verbeek and Binoy Ravindran},
title = {Formally Verified Big Step Semantics out of x86-64 Binaries},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {241-240},
doi = {10.1145/3293880.3294102},
year = {2019},
}
Publisher's Version
Article: poplws19cppmain-id20-p doi:10.1145/3293880.3294102
|
| |
Winterhalter, Théo
|
CPP '19: "Eliminating Reflection from ..."
Eliminating Reflection from Type Theory
Théo Winterhalter, Matthieu Sozeau, and Nicolas Tabareau
(Inria, France)
@InProceedings{CPP19p122,
author = {Théo Winterhalter and Matthieu Sozeau and Nicolas Tabareau},
title = {Eliminating Reflection from Type Theory},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {122-121},
doi = {10.1145/3293880.3294095},
year = {2019},
}
Publisher's Version
Article: poplws19cppmain-id30-p doi:10.1145/3293880.3294095
|
| |
Xia, Li-yao
|
CPP '19: "From C to Interaction Trees: ..."
From C to Interaction Trees: Specifying, Verifying, and Testing a Networked Server
Nicolas Koh, Yao Li, Yishuai Li, Li-yao Xia, Lennart Beringer, Wolf Honoré, William Mansky, Benjamin C. Pierce, and Steve Zdancewic
(University of Pennsylvania, USA; Princeton University, USA; Yale University, USA; University of Illinois at Chicago, USA)
@InProceedings{CPP19p309,
author = {Nicolas Koh and Yao Li and Yishuai Li and Li-yao Xia and Lennart Beringer and Wolf Honoré and William Mansky and Benjamin C. Pierce and Steve Zdancewic},
title = {From C to Interaction Trees: Specifying, Verifying, and Testing a Networked Server},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {309-308},
doi = {10.1145/3293880.3294106},
year = {2019},
}
Publisher's Version
Article: poplws19cppmain-id22-p doi:10.1145/3293880.3294106
|
| |
Ye, Qianchuan
|
CPP '19: "A Verified Protocol Buffer ..."
A Verified Protocol Buffer Compiler
Qianchuan Ye and Benjamin Delaware
(Purdue University, USA)
@InProceedings{CPP19p292,
author = {Qianchuan Ye and Benjamin Delaware},
title = {A Verified Protocol Buffer Compiler},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {292-291},
doi = {10.1145/3293880.3294105},
year = {2019},
}
Publisher's Version
Published Artifact
Artifacts Available
Article: poplws19cppmain-id21-p doi:10.1145/3293880.3294105
|
| |
Zdancewic, Steve
|
CPP '19: "From C to Interaction Trees: ..."
From C to Interaction Trees: Specifying, Verifying, and Testing a Networked Server
Nicolas Koh, Yao Li, Yishuai Li, Li-yao Xia, Lennart Beringer, Wolf Honoré, William Mansky, Benjamin C. Pierce, and Steve Zdancewic
(University of Pennsylvania, USA; Princeton University, USA; Yale University, USA; University of Illinois at Chicago, USA)
@InProceedings{CPP19p309,
author = {Nicolas Koh and Yao Li and Yishuai Li and Li-yao Xia and Lennart Beringer and Wolf Honoré and William Mansky and Benjamin C. Pierce and Steve Zdancewic},
title = {From C to Interaction Trees: Specifying, Verifying, and Testing a Networked Server},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {309-308},
doi = {10.1145/3293880.3294106},
year = {2019},
}
Publisher's Version
Article: poplws19cppmain-id22-p doi:10.1145/3293880.3294106
|
| |
Zhan, Bohua |
CPP '19: "Smooth Manifolds and Types ..."
Smooth Manifolds and Types to Sets for Linear Algebra in Isabelle/HOL
Fabian Immler and Bohua Zhan
(Carnegie Mellon University, USA; Institute of Software at Chinese Academy of Sciences, China)
@InProceedings{CPP19p88,
author = {Fabian Immler and Bohua Zhan},
title = {Smooth Manifolds and Types to Sets for Linear Algebra in Isabelle/HOL},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {88-87},
doi = {10.1145/3293880.3294093},
year = {2019},
}
Publisher's Version
Article: poplws19cppmain-id10-p doi:10.1145/3293880.3294093
|