Workshop CPP 2019 – Author Index

B C D E F G H I K L M P R S T V W X Y Z

	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
	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
	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 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
	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
	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
	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
	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
	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
	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
	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
	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 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 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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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
	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 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
	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
	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
	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
	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
	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 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
	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
	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
	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
	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
	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
	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
	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
	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
	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

55 authors

proc time: 0.05