| |
Amani, Sidney
|
CPP '18: "Towards Verifying Ethereum ..."
Towards Verifying Ethereum Smart Contract Bytecode in Isabelle/HOL
Sidney Amani, Myriam Bégel, Maksym Bortin, and Mark Staples
(Data61 at CSIRO, Australia; ENS Paris-Saclay, France; University of Paris-Saclay, France; UNSW, Australia)
@InProceedings{CPP18p97,
author = {Sidney Amani and Myriam Bégel and Maksym Bortin and Mark Staples},
title = {Towards Verifying Ethereum Smart Contract Bytecode in Isabelle/HOL},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {97-96},
doi = {10.1145/3167084},
year = {2018},
}
 Publisher's Version
Article: poplws18cppmain-id25-p doi:10.1145/3167084
|
| |
Bard, Joachim
|
CPP '18: "Completeness and Decidability ..."
Completeness and Decidability of Converse PDL in the Constructive Type Theory of Coq
Christian Doczkal and Joachim Bard
(University of Lyon, France; CNRS, France; ENS Lyon, France; Claude Bernard University Lyon 1, France; LIP, France; Saarland University, Germany)
@InProceedings{CPP18p65,
author = {Christian Doczkal and Joachim Bard},
title = {Completeness and Decidability of Converse PDL in the Constructive Type Theory of Coq},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {65-64},
doi = {10.1145/3167088},
year = {2018},
}
Publisher's Version
Article: poplws18cppmain-id42-p doi:10.1145/3167088
|
| |
Bégel, Myriam |
CPP '18: "Towards Verifying Ethereum ..."
Towards Verifying Ethereum Smart Contract Bytecode in Isabelle/HOL
Sidney Amani, Myriam Bégel, Maksym Bortin, and Mark Staples
(Data61 at CSIRO, Australia; ENS Paris-Saclay, France; University of Paris-Saclay, France; UNSW, Australia)
@InProceedings{CPP18p97,
author = {Sidney Amani and Myriam Bégel and Maksym Bortin and Mark Staples},
title = {Towards Verifying Ethereum Smart Contract Bytecode in Isabelle/HOL},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {97-96},
doi = {10.1145/3167084},
year = {2018},
}
Publisher's Version
Article: poplws18cppmain-id25-p doi:10.1145/3167084
|
| |
Biernacki, Dariusz |
CPP '18: "A Coq Formalization of Normalization ..."
A Coq Formalization of Normalization by Evaluation for Martin-Löf Type Theory
Paweł Wieczorek and Dariusz Biernacki
(University of Wrocław, Poland)
@InProceedings{CPP18p337,
author = {Paweł Wieczorek and Dariusz Biernacki},
title = {A Coq Formalization of Normalization by Evaluation for Martin-Löf Type Theory},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {337-336},
doi = {10.1145/3167091},
year = {2018},
}
Publisher's Version
Article: poplws18cppmain-id37-p doi:10.1145/3167091
|
| |
Blanchette, Jasmin Christian |
CPP '18: "A Verified SAT Solver with ..."
A Verified SAT Solver with Watched Literals Using Imperative HOL
Mathias Fleury, Jasmin Christian Blanchette, and Peter Lammich
(Max Planck Institute for Informatics, Germany; Vrije Universiteit Amsterdam, Netherlands; TU Munich, Germany; Virginia Tech, USA)
@InProceedings{CPP18p209,
author = {Mathias Fleury and Jasmin Christian Blanchette and Peter Lammich},
title = {A Verified SAT Solver with Watched Literals Using Imperative HOL},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {209-208},
doi = {10.1145/3167080},
year = {2018},
}
Publisher's Version
Article: poplws18cppmain-id7-p doi:10.1145/3167080
|
| |
Bonacina, Maria Paola |
CPP '18: "Proofs in Conflict-Driven ..."
Proofs in Conflict-Driven Theory Combination
Maria Paola Bonacina, Stéphane Graham-Lengrand, and Natarajan Shankar
(University of Verona, Italy; CNRS, France; Inria, France; École Polytechnique, France; SRI International, USA)
@InProceedings{CPP18p241,
author = {Maria Paola Bonacina and Stéphane Graham-Lengrand and Natarajan Shankar},
title = {Proofs in Conflict-Driven Theory Combination},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {241-240},
doi = {10.1145/3167096},
year = {2018},
}
Publisher's Version
Article: poplws18cppmain-id32-p doi:10.1145/3167096
|
| |
Bortin, Maksym |
CPP '18: "Towards Verifying Ethereum ..."
Towards Verifying Ethereum Smart Contract Bytecode in Isabelle/HOL
Sidney Amani, Myriam Bégel, Maksym Bortin, and Mark Staples
(Data61 at CSIRO, Australia; ENS Paris-Saclay, France; University of Paris-Saclay, France; UNSW, Australia)
@InProceedings{CPP18p97,
author = {Sidney Amani and Myriam Bégel and Maksym Bortin and Mark Staples},
title = {Towards Verifying Ethereum Smart Contract Bytecode in Isabelle/HOL},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {97-96},
doi = {10.1145/3167084},
year = {2018},
}
Publisher's Version
Article: poplws18cppmain-id25-p doi:10.1145/3167084
|
| |
Breitner, Joachim |
CPP '18: "Total Haskell is Reasonable ..."
Total Haskell is Reasonable Coq
Antal Spector-Zabusky, Joachim Breitner, Christine Rizkallah, and Stephanie Weirich
(University of Pennsylvania, USA)
@InProceedings{CPP18p33,
author = {Antal Spector-Zabusky and Joachim Breitner and Christine Rizkallah and Stephanie Weirich},
title = {Total Haskell is Reasonable Coq},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {33-32},
doi = {10.1145/3167092},
year = {2018},
}
Publisher's Version
Article: poplws18cppmain-id51-p doi:10.1145/3167092
|
| |
Chaudhuri, Kaustuv
|
CPP '18: "A Two-Level Logic Perspective ..."
A Two-Level Logic Perspective on (Simultaneous) Substitutions
Kaustuv Chaudhuri
(Inria, France; École Polytechnique, France)
@InProceedings{CPP18p353,
author = {Kaustuv Chaudhuri},
title = {A Two-Level Logic Perspective on (Simultaneous) Substitutions},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {353-352},
doi = {10.1145/3167093},
year = {2018},
}
Publisher's Version
Article: poplws18cppmain-id59-p doi:10.1145/3167093
|
| |
Divasón, Jose
|
CPP '18: "Efficient Certification of ..."
Efficient Certification of Complexity Proofs: Formalizing the Perron–Frobenius Theorem (Invited Talk Paper)
Jose Divasón, Sebastiaan Joosten, Ondřej Kunčar, René Thiemann, and Akihisa Yamada
(University of La Rioja, Spain; University of Twente, Netherlands; TU Munich, Germany; University of Innsbruck, Austria; National Institute of Informatics, Japan)
@InProceedings{CPP18p17,
author = {Jose Divasón and Sebastiaan Joosten and Ondřej Kunčar and René Thiemann and Akihisa Yamada},
title = {Efficient Certification of Complexity Proofs: Formalizing the Perron–Frobenius Theorem (Invited Talk Paper)},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {17-16},
doi = {},
year = {2018},
}
Article: poplws18cppmain-id101-p doi:
|
| |
Djalal, Boris |
CPP '18: "A Constructive Formalisation ..."
A Constructive Formalisation of Semi-algebraic Sets and Functions
Boris Djalal
(Inria, France)
@InProceedings{CPP18p305,
author = {Boris Djalal},
title = {A Constructive Formalisation of Semi-algebraic Sets and Functions},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {305-304},
doi = {10.1145/3167099},
year = {2018},
}
Publisher's Version
Article: poplws18cppmain-id19-p doi:10.1145/3167099
|
| |
Doczkal, Christian |
CPP '18: "Completeness and Decidability ..."
Completeness and Decidability of Converse PDL in the Constructive Type Theory of Coq
Christian Doczkal and Joachim Bard
(University of Lyon, France; CNRS, France; ENS Lyon, France; Claude Bernard University Lyon 1, France; LIP, France; Saarland University, Germany)
@InProceedings{CPP18p65,
author = {Christian Doczkal and Joachim Bard},
title = {Completeness and Decidability of Converse PDL in the Constructive Type Theory of Coq},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {65-64},
doi = {10.1145/3167088},
year = {2018},
}
Publisher's Version
Article: poplws18cppmain-id42-p doi:10.1145/3167088
|
| |
Férée, Hugo
|
CPP '18: "Formal Proof of Polynomial-Time ..."
Formal Proof of Polynomial-Time Complexity with Quasi-Interpretations
Hugo Férée, Samuel Hym, Micaela Mayero, Jean-Yves Moyen, and David Nowak
(University of Kent, UK; University of Lille, France; University of Paris 13, France; University of Copenhagen, Denmark; CNRS, France)
@InProceedings{CPP18p193,
author = {Hugo Férée and Samuel Hym and Micaela Mayero and Jean-Yves Moyen and David Nowak},
title = {Formal Proof of Polynomial-Time Complexity with Quasi-Interpretations},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {193-192},
doi = {10.1145/3167097},
year = {2018},
}
Publisher's Version
Article: poplws18cppmain-id39-p doi:10.1145/3167097
|
| |
Firsov, Denis |
CPP '18: "Generic Derivation of Induction ..."
Generic Derivation of Induction for Impredicative Encodings in Cedille
Denis Firsov and Aaron Stump
(University of Iowa, USA)
@InProceedings{CPP18p273,
author = {Denis Firsov and Aaron Stump},
title = {Generic Derivation of Induction for Impredicative Encodings in Cedille},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {273-272},
doi = {10.1145/3167087},
year = {2018},
}
Publisher's Version
Article: poplws18cppmain-id49-p doi:10.1145/3167087
|
| |
Fleury, Mathias |
CPP '18: "A Verified SAT Solver with ..."
A Verified SAT Solver with Watched Literals Using Imperative HOL
Mathias Fleury, Jasmin Christian Blanchette, and Peter Lammich
(Max Planck Institute for Informatics, Germany; Vrije Universiteit Amsterdam, Netherlands; TU Munich, Germany; Virginia Tech, USA)
@InProceedings{CPP18p209,
author = {Mathias Fleury and Jasmin Christian Blanchette and Peter Lammich},
title = {A Verified SAT Solver with Watched Literals Using Imperative HOL},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {209-208},
doi = {10.1145/3167080},
year = {2018},
}
Publisher's Version
Article: poplws18cppmain-id7-p doi:10.1145/3167080
|
| |
Fournet, Cédric |
CPP '18: "A Monadic Framework for Relational ..."
A Monadic Framework for Relational Verification: Applied to Information Security, Program Equivalence, and Optimizations
Niklas Grimm, Kenji Maillard, Cédric Fournet, Cătălin Hriţcu, Matteo Maffei, Jonathan Protzenko, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy, and Santiago Zanella-Béguelin
(Vienna University of Technology, Austria; Inria, France; ENS Paris, France; Microsoft Research, UK; Microsoft Research, USA; Microsoft Research, India)
@InProceedings{CPP18p177,
author = {Niklas Grimm and Kenji Maillard and Cédric Fournet and Cătălin Hriţcu and Matteo Maffei and Jonathan Protzenko and Tahina Ramananandro and Aseem Rastogi and Nikhil Swamy and Santiago Zanella-Béguelin},
title = {A Monadic Framework for Relational Verification: Applied to Information Security, Program Equivalence, and Optimizations},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {177-176},
doi = {10.1145/3167090},
year = {2018},
}
Publisher's Version
Article: poplws18cppmain-id14-p doi:10.1145/3167090
|
| |
Frumin, Dan |
CPP '18: "Finite Sets in Homotopy Type ..."
Finite Sets in Homotopy Type Theory
Dan Frumin, Herman Geuvers, Léon Gondelman, and Niels van der Weide
(Radboud University Nijmegen, Netherlands)
@InProceedings{CPP18p257,
author = {Dan Frumin and Herman Geuvers and Léon Gondelman and Niels van der Weide},
title = {Finite Sets in Homotopy Type Theory},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {257-256},
doi = {10.1145/3167085},
year = {2018},
}
Publisher's Version
Article: poplws18cppmain-id38-p doi:10.1145/3167085
|
| |
Geuvers, Herman
|
CPP '18: "Finite Sets in Homotopy Type ..."
Finite Sets in Homotopy Type Theory
Dan Frumin, Herman Geuvers, Léon Gondelman, and Niels van der Weide
(Radboud University Nijmegen, Netherlands)
@InProceedings{CPP18p257,
author = {Dan Frumin and Herman Geuvers and Léon Gondelman and Niels van der Weide},
title = {Finite Sets in Homotopy Type Theory},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {257-256},
doi = {10.1145/3167085},
year = {2018},
}
Publisher's Version
Article: poplws18cppmain-id38-p doi:10.1145/3167085
|
| |
Gondelman, Léon |
CPP '18: "Finite Sets in Homotopy Type ..."
Finite Sets in Homotopy Type Theory
Dan Frumin, Herman Geuvers, Léon Gondelman, and Niels van der Weide
(Radboud University Nijmegen, Netherlands)
@InProceedings{CPP18p257,
author = {Dan Frumin and Herman Geuvers and Léon Gondelman and Niels van der Weide},
title = {Finite Sets in Homotopy Type Theory},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {257-256},
doi = {10.1145/3167085},
year = {2018},
}
Publisher's Version
Article: poplws18cppmain-id38-p doi:10.1145/3167085
|
| |
Graham-Lengrand, Stéphane |
CPP '18: "Proofs in Conflict-Driven ..."
Proofs in Conflict-Driven Theory Combination
Maria Paola Bonacina, Stéphane Graham-Lengrand, and Natarajan Shankar
(University of Verona, Italy; CNRS, France; Inria, France; École Polytechnique, France; SRI International, USA)
@InProceedings{CPP18p241,
author = {Maria Paola Bonacina and Stéphane Graham-Lengrand and Natarajan Shankar},
title = {Proofs in Conflict-Driven Theory Combination},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {241-240},
doi = {10.1145/3167096},
year = {2018},
}
Publisher's Version
Article: poplws18cppmain-id32-p doi:10.1145/3167096
|
| |
Grimm, Niklas |
CPP '18: "A Monadic Framework for Relational ..."
A Monadic Framework for Relational Verification: Applied to Information Security, Program Equivalence, and Optimizations
Niklas Grimm, Kenji Maillard, Cédric Fournet, Cătălin Hriţcu, Matteo Maffei, Jonathan Protzenko, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy, and Santiago Zanella-Béguelin
(Vienna University of Technology, Austria; Inria, France; ENS Paris, France; Microsoft Research, UK; Microsoft Research, USA; Microsoft Research, India)
@InProceedings{CPP18p177,
author = {Niklas Grimm and Kenji Maillard and Cédric Fournet and Cătălin Hriţcu and Matteo Maffei and Jonathan Protzenko and Tahina Ramananandro and Aseem Rastogi and Nikhil Swamy and Santiago Zanella-Béguelin},
title = {A Monadic Framework for Relational Verification: Applied to Information Security, Program Equivalence, and Optimizations},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {177-176},
doi = {10.1145/3167090},
year = {2018},
}
Publisher's Version
Article: poplws18cppmain-id14-p doi:10.1145/3167090
|
| |
Grossman, Dan |
CPP '18: "Adapting Proof Automation ..."
Adapting Proof Automation to Adapt Proofs
Talia Ringer, Nathaniel Yazdani, John Leo, and Dan Grossman
(University of Washington, USA; Halfaya Research, USA)
@InProceedings{CPP18p161,
author = {Talia Ringer and Nathaniel Yazdani and John Leo and Dan Grossman},
title = {Adapting Proof Automation to Adapt Proofs},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {161-160},
doi = {10.1145/3167094},
year = {2018},
}
Publisher's Version
Article: poplws18cppmain-id23-p doi:10.1145/3167094
CPP '18: "Œuf: Minimizing the Coq Extraction ..."
Œuf: Minimizing the Coq Extraction TCB
Eric Mullen, Stuart Pernsteiner, James R. Wilcox, Zachary Tatlock, and Dan Grossman
(University of Washington, USA)
@InProceedings{CPP18p225,
author = {Eric Mullen and Stuart Pernsteiner and James R. Wilcox and Zachary Tatlock and Dan Grossman},
title = {Œuf: Minimizing the Coq Extraction TCB},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {225-224},
doi = {10.1145/3167089},
year = {2018},
}
Publisher's Version
Article: poplws18cppmain-id12-p doi:10.1145/3167089
|
| |
Hriţcu, Cătălin
|
CPP '18: "A Monadic Framework for Relational ..."
A Monadic Framework for Relational Verification: Applied to Information Security, Program Equivalence, and Optimizations
Niklas Grimm, Kenji Maillard, Cédric Fournet, Cătălin Hriţcu, Matteo Maffei, Jonathan Protzenko, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy, and Santiago Zanella-Béguelin
(Vienna University of Technology, Austria; Inria, France; ENS Paris, France; Microsoft Research, UK; Microsoft Research, USA; Microsoft Research, India)
@InProceedings{CPP18p177,
author = {Niklas Grimm and Kenji Maillard and Cédric Fournet and Cătălin Hriţcu and Matteo Maffei and Jonathan Protzenko and Tahina Ramananandro and Aseem Rastogi and Nikhil Swamy and Santiago Zanella-Béguelin},
title = {A Monadic Framework for Relational Verification: Applied to Information Security, Program Equivalence, and Optimizations},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {177-176},
doi = {10.1145/3167090},
year = {2018},
}
Publisher's Version
Article: poplws18cppmain-id14-p doi:10.1145/3167090
|
| |
Hym, Samuel |
CPP '18: "Formal Proof of Polynomial-Time ..."
Formal Proof of Polynomial-Time Complexity with Quasi-Interpretations
Hugo Férée, Samuel Hym, Micaela Mayero, Jean-Yves Moyen, and David Nowak
(University of Kent, UK; University of Lille, France; University of Paris 13, France; University of Copenhagen, Denmark; CNRS, France)
@InProceedings{CPP18p193,
author = {Hugo Férée and Samuel Hym and Micaela Mayero and Jean-Yves Moyen and David Nowak},
title = {Formal Proof of Polynomial-Time Complexity with Quasi-Interpretations},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {193-192},
doi = {10.1145/3167097},
year = {2018},
}
Publisher's Version
Article: poplws18cppmain-id39-p doi:10.1145/3167097
|
| |
Joosten, Sebastiaan
|
CPP '18: "Efficient Certification of ..."
Efficient Certification of Complexity Proofs: Formalizing the Perron–Frobenius Theorem (Invited Talk Paper)
Jose Divasón, Sebastiaan Joosten, Ondřej Kunčar, René Thiemann, and Akihisa Yamada
(University of La Rioja, Spain; University of Twente, Netherlands; TU Munich, Germany; University of Innsbruck, Austria; National Institute of Informatics, Japan)
@InProceedings{CPP18p17,
author = {Jose Divasón and Sebastiaan Joosten and Ondřej Kunčar and René Thiemann and Akihisa Yamada},
title = {Efficient Certification of Complexity Proofs: Formalizing the Perron–Frobenius Theorem (Invited Talk Paper)},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {17-16},
doi = {},
year = {2018},
}
Article: poplws18cppmain-id101-p doi:
|
| |
Kaiser, Jonas
|
CPP '18: "Binder Aware Recursion over ..."
Binder Aware Recursion over Well-Scoped de Bruijn Syntax
Jonas Kaiser, Steven Schäfer, and Kathrin Stark
(Saarland University, Germany)
@InProceedings{CPP18p369,
author = {Jonas Kaiser and Steven Schäfer and Kathrin Stark},
title = {Binder Aware Recursion over Well-Scoped de Bruijn Syntax},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {369-368},
doi = {10.1145/3167098},
year = {2018},
}
Publisher's Version
Article: poplws18cppmain-id60-p doi:10.1145/3167098
|
| |
Kaliszyk, Cezary |
CPP '18: "Formal Microeconomic Foundations ..."
Formal Microeconomic Foundations and the First Welfare Theorem
Cezary Kaliszyk and Julian Parsert
(University of Innsbruck, Austria)
@InProceedings{CPP18p129,
author = {Cezary Kaliszyk and Julian Parsert},
title = {Formal Microeconomic Foundations and the First Welfare Theorem},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {129-128},
doi = {10.1145/3167100},
year = {2018},
}
Publisher's Version
Article: poplws18cppmain-id29-p doi:10.1145/3167100
|
| |
Kirst, Dominik |
CPP '18: "Large Model Constructions ..."
Large Model Constructions for Second-Order ZF in Dependent Type Theory
Dominik Kirst and Gert Smolka
(Saarland University, Germany)
@InProceedings{CPP18p289,
author = {Dominik Kirst and Gert Smolka},
title = {Large Model Constructions for Second-Order ZF in Dependent Type Theory},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {289-288},
doi = {10.1145/3167095},
year = {2018},
}
Publisher's Version
Article: poplws18cppmain-id8-p doi:10.1145/3167095
|
| |
Kunčar, Ondřej |
CPP '18: "Efficient Certification of ..."
Efficient Certification of Complexity Proofs: Formalizing the Perron–Frobenius Theorem (Invited Talk Paper)
Jose Divasón, Sebastiaan Joosten, Ondřej Kunčar, René Thiemann, and Akihisa Yamada
(University of La Rioja, Spain; University of Twente, Netherlands; TU Munich, Germany; University of Innsbruck, Austria; National Institute of Informatics, Japan)
@InProceedings{CPP18p17,
author = {Jose Divasón and Sebastiaan Joosten and Ondřej Kunčar and René Thiemann and Akihisa Yamada},
title = {Efficient Certification of Complexity Proofs: Formalizing the Perron–Frobenius Theorem (Invited Talk Paper)},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {17-16},
doi = {},
year = {2018},
}
Article: poplws18cppmain-id101-p doi:
|
| |
Lammich, Peter
|
CPP '18: "A Verified SAT Solver with ..."
A Verified SAT Solver with Watched Literals Using Imperative HOL
Mathias Fleury, Jasmin Christian Blanchette, and Peter Lammich
(Max Planck Institute for Informatics, Germany; Vrije Universiteit Amsterdam, Netherlands; TU Munich, Germany; Virginia Tech, USA)
@InProceedings{CPP18p209,
author = {Mathias Fleury and Jasmin Christian Blanchette and Peter Lammich},
title = {A Verified SAT Solver with Watched Literals Using Imperative HOL},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {209-208},
doi = {10.1145/3167080},
year = {2018},
}
Publisher's Version
Article: poplws18cppmain-id7-p doi:10.1145/3167080
|
| |
Lenglet, Sergueï |
CPP '18: "HOπ in Coq ..."
HOπ in Coq
Sergueï Lenglet and Alan Schmitt
(University of Lorraine, France; Inria, France)
@InProceedings{CPP18p321,
author = {Sergueï Lenglet and Alan Schmitt},
title = {HOπ in Coq},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {321-320},
doi = {10.1145/3167083},
year = {2018},
}
Publisher's Version
Article: poplws18cppmain-id18-p doi:10.1145/3167083
|
| |
Leo, John |
CPP '18: "Adapting Proof Automation ..."
Adapting Proof Automation to Adapt Proofs
Talia Ringer, Nathaniel Yazdani, John Leo, and Dan Grossman
(University of Washington, USA; Halfaya Research, USA)
@InProceedings{CPP18p161,
author = {Talia Ringer and Nathaniel Yazdani and John Leo and Dan Grossman},
title = {Adapting Proof Automation to Adapt Proofs},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {161-160},
doi = {10.1145/3167094},
year = {2018},
}
Publisher's Version
Article: poplws18cppmain-id23-p doi:10.1145/3167094
|
| |
Maffei, Matteo
|
CPP '18: "A Monadic Framework for Relational ..."
A Monadic Framework for Relational Verification: Applied to Information Security, Program Equivalence, and Optimizations
Niklas Grimm, Kenji Maillard, Cédric Fournet, Cătălin Hriţcu, Matteo Maffei, Jonathan Protzenko, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy, and Santiago Zanella-Béguelin
(Vienna University of Technology, Austria; Inria, France; ENS Paris, France; Microsoft Research, UK; Microsoft Research, USA; Microsoft Research, India)
@InProceedings{CPP18p177,
author = {Niklas Grimm and Kenji Maillard and Cédric Fournet and Cătălin Hriţcu and Matteo Maffei and Jonathan Protzenko and Tahina Ramananandro and Aseem Rastogi and Nikhil Swamy and Santiago Zanella-Béguelin},
title = {A Monadic Framework for Relational Verification: Applied to Information Security, Program Equivalence, and Optimizations},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {177-176},
doi = {10.1145/3167090},
year = {2018},
}
Publisher's Version
Article: poplws18cppmain-id14-p doi:10.1145/3167090
|
| |
Maillard, Kenji |
CPP '18: "A Monadic Framework for Relational ..."
A Monadic Framework for Relational Verification: Applied to Information Security, Program Equivalence, and Optimizations
Niklas Grimm, Kenji Maillard, Cédric Fournet, Cătălin Hriţcu, Matteo Maffei, Jonathan Protzenko, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy, and Santiago Zanella-Béguelin
(Vienna University of Technology, Austria; Inria, France; ENS Paris, France; Microsoft Research, UK; Microsoft Research, USA; Microsoft Research, India)
@InProceedings{CPP18p177,
author = {Niklas Grimm and Kenji Maillard and Cédric Fournet and Cătălin Hriţcu and Matteo Maffei and Jonathan Protzenko and Tahina Ramananandro and Aseem Rastogi and Nikhil Swamy and Santiago Zanella-Béguelin},
title = {A Monadic Framework for Relational Verification: Applied to Information Security, Program Equivalence, and Optimizations},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {177-176},
doi = {10.1145/3167090},
year = {2018},
}
Publisher's Version
Article: poplws18cppmain-id14-p doi:10.1145/3167090
|
| |
Mayero, Micaela |
CPP '18: "Formal Proof of Polynomial-Time ..."
Formal Proof of Polynomial-Time Complexity with Quasi-Interpretations
Hugo Férée, Samuel Hym, Micaela Mayero, Jean-Yves Moyen, and David Nowak
(University of Kent, UK; University of Lille, France; University of Paris 13, France; University of Copenhagen, Denmark; CNRS, France)
@InProceedings{CPP18p193,
author = {Hugo Férée and Samuel Hym and Micaela Mayero and Jean-Yves Moyen and David Nowak},
title = {Formal Proof of Polynomial-Time Complexity with Quasi-Interpretations},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {193-192},
doi = {10.1145/3167097},
year = {2018},
}
Publisher's Version
Article: poplws18cppmain-id39-p doi:10.1145/3167097
|
| |
McKinna, James |
CPP '18: "Triangulating Context Lemmas ..."
Triangulating Context Lemmas
Craig McLaughlin, James McKinna, and Ian Stark
(University of Edinburgh, UK)
@InProceedings{CPP18p145,
author = {Craig McLaughlin and James McKinna and Ian Stark},
title = {Triangulating Context Lemmas},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {145-144},
doi = {10.1145/3167081},
year = {2018},
}
Publisher's Version
Article: poplws18cppmain-id2-p doi:10.1145/3167081
|
| |
McLaughlin, Craig |
CPP '18: "Triangulating Context Lemmas ..."
Triangulating Context Lemmas
Craig McLaughlin, James McKinna, and Ian Stark
(University of Edinburgh, UK)
@InProceedings{CPP18p145,
author = {Craig McLaughlin and James McKinna and Ian Stark},
title = {Triangulating Context Lemmas},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {145-144},
doi = {10.1145/3167081},
year = {2018},
}
Publisher's Version
Article: poplws18cppmain-id2-p doi:10.1145/3167081
|
| |
Moyen, Jean-Yves |
CPP '18: "Formal Proof of Polynomial-Time ..."
Formal Proof of Polynomial-Time Complexity with Quasi-Interpretations
Hugo Férée, Samuel Hym, Micaela Mayero, Jean-Yves Moyen, and David Nowak
(University of Kent, UK; University of Lille, France; University of Paris 13, France; University of Copenhagen, Denmark; CNRS, France)
@InProceedings{CPP18p193,
author = {Hugo Férée and Samuel Hym and Micaela Mayero and Jean-Yves Moyen and David Nowak},
title = {Formal Proof of Polynomial-Time Complexity with Quasi-Interpretations},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {193-192},
doi = {10.1145/3167097},
year = {2018},
}
Publisher's Version
Article: poplws18cppmain-id39-p doi:10.1145/3167097
|
| |
Mullen, Eric |
CPP '18: "Œuf: Minimizing the Coq Extraction ..."
Œuf: Minimizing the Coq Extraction TCB
Eric Mullen, Stuart Pernsteiner, James R. Wilcox, Zachary Tatlock, and Dan Grossman
(University of Washington, USA)
@InProceedings{CPP18p225,
author = {Eric Mullen and Stuart Pernsteiner and James R. Wilcox and Zachary Tatlock and Dan Grossman},
title = {Œuf: Minimizing the Coq Extraction TCB},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {225-224},
doi = {10.1145/3167089},
year = {2018},
}
Publisher's Version
Article: poplws18cppmain-id12-p doi:10.1145/3167089
|
| |
Nowak, David
|
CPP '18: "Formal Proof of Polynomial-Time ..."
Formal Proof of Polynomial-Time Complexity with Quasi-Interpretations
Hugo Férée, Samuel Hym, Micaela Mayero, Jean-Yves Moyen, and David Nowak
(University of Kent, UK; University of Lille, France; University of Paris 13, France; University of Copenhagen, Denmark; CNRS, France)
@InProceedings{CPP18p193,
author = {Hugo Férée and Samuel Hym and Micaela Mayero and Jean-Yves Moyen and David Nowak},
title = {Formal Proof of Polynomial-Time Complexity with Quasi-Interpretations},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {193-192},
doi = {10.1145/3167097},
year = {2018},
}
Publisher's Version
Article: poplws18cppmain-id39-p doi:10.1145/3167097
|
| |
Parsert, Julian
|
CPP '18: "Formal Microeconomic Foundations ..."
Formal Microeconomic Foundations and the First Welfare Theorem
Cezary Kaliszyk and Julian Parsert
(University of Innsbruck, Austria)
@InProceedings{CPP18p129,
author = {Cezary Kaliszyk and Julian Parsert},
title = {Formal Microeconomic Foundations and the First Welfare Theorem},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {129-128},
doi = {10.1145/3167100},
year = {2018},
}
Publisher's Version
Article: poplws18cppmain-id29-p doi:10.1145/3167100
|
| |
Pernsteiner, Stuart |
CPP '18: "Œuf: Minimizing the Coq Extraction ..."
Œuf: Minimizing the Coq Extraction TCB
Eric Mullen, Stuart Pernsteiner, James R. Wilcox, Zachary Tatlock, and Dan Grossman
(University of Washington, USA)
@InProceedings{CPP18p225,
author = {Eric Mullen and Stuart Pernsteiner and James R. Wilcox and Zachary Tatlock and Dan Grossman},
title = {Œuf: Minimizing the Coq Extraction TCB},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {225-224},
doi = {10.1145/3167089},
year = {2018},
}
Publisher's Version
Article: poplws18cppmain-id12-p doi:10.1145/3167089
|
| |
Pientka, Brigitte |
CPP '18: "POPLMark Reloaded: Mechanizing ..."
POPLMark Reloaded: Mechanizing Logical Relations Proofs (Invited Talk)
Brigitte Pientka
(McGill University, Canada)
@InProceedings{CPP18p1,
author = {Brigitte Pientka},
title = {POPLMark Reloaded: Mechanizing Logical Relations Proofs (Invited Talk)},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {1-0},
doi = {10.1145/3167102},
year = {2018},
}
Publisher's Version
Article: poplws18cppmain-id100-p doi:10.1145/3167102
|
| |
Pîrlea, George |
CPP '18: "Mechanising Blockchain Consensus ..."
Mechanising Blockchain Consensus
George Pîrlea and Ilya Sergey
(University College London, UK)
@InProceedings{CPP18p113,
author = {George Pîrlea and Ilya Sergey},
title = {Mechanising Blockchain Consensus},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {113-112},
doi = {10.1145/3167086},
year = {2018},
}
Publisher's Version
Article: poplws18cppmain-id48-p doi:10.1145/3167086
|
| |
Protzenko, Jonathan |
CPP '18: "A Monadic Framework for Relational ..."
A Monadic Framework for Relational Verification: Applied to Information Security, Program Equivalence, and Optimizations
Niklas Grimm, Kenji Maillard, Cédric Fournet, Cătălin Hriţcu, Matteo Maffei, Jonathan Protzenko, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy, and Santiago Zanella-Béguelin
(Vienna University of Technology, Austria; Inria, France; ENS Paris, France; Microsoft Research, UK; Microsoft Research, USA; Microsoft Research, India)
@InProceedings{CPP18p177,
author = {Niklas Grimm and Kenji Maillard and Cédric Fournet and Cătălin Hriţcu and Matteo Maffei and Jonathan Protzenko and Tahina Ramananandro and Aseem Rastogi and Nikhil Swamy and Santiago Zanella-Béguelin},
title = {A Monadic Framework for Relational Verification: Applied to Information Security, Program Equivalence, and Optimizations},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {177-176},
doi = {10.1145/3167090},
year = {2018},
}
Publisher's Version
Article: poplws18cppmain-id14-p doi:10.1145/3167090
|
| |
Ramananandro, Tahina
|
CPP '18: "A Monadic Framework for Relational ..."
A Monadic Framework for Relational Verification: Applied to Information Security, Program Equivalence, and Optimizations
Niklas Grimm, Kenji Maillard, Cédric Fournet, Cătălin Hriţcu, Matteo Maffei, Jonathan Protzenko, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy, and Santiago Zanella-Béguelin
(Vienna University of Technology, Austria; Inria, France; ENS Paris, France; Microsoft Research, UK; Microsoft Research, USA; Microsoft Research, India)
@InProceedings{CPP18p177,
author = {Niklas Grimm and Kenji Maillard and Cédric Fournet and Cătălin Hriţcu and Matteo Maffei and Jonathan Protzenko and Tahina Ramananandro and Aseem Rastogi and Nikhil Swamy and Santiago Zanella-Béguelin},
title = {A Monadic Framework for Relational Verification: Applied to Information Security, Program Equivalence, and Optimizations},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {177-176},
doi = {10.1145/3167090},
year = {2018},
}
Publisher's Version
Article: poplws18cppmain-id14-p doi:10.1145/3167090
|
| |
Rastogi, Aseem |
CPP '18: "A Monadic Framework for Relational ..."
A Monadic Framework for Relational Verification: Applied to Information Security, Program Equivalence, and Optimizations
Niklas Grimm, Kenji Maillard, Cédric Fournet, Cătălin Hriţcu, Matteo Maffei, Jonathan Protzenko, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy, and Santiago Zanella-Béguelin
(Vienna University of Technology, Austria; Inria, France; ENS Paris, France; Microsoft Research, UK; Microsoft Research, USA; Microsoft Research, India)
@InProceedings{CPP18p177,
author = {Niklas Grimm and Kenji Maillard and Cédric Fournet and Cătălin Hriţcu and Matteo Maffei and Jonathan Protzenko and Tahina Ramananandro and Aseem Rastogi and Nikhil Swamy and Santiago Zanella-Béguelin},
title = {A Monadic Framework for Relational Verification: Applied to Information Security, Program Equivalence, and Optimizations},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {177-176},
doi = {10.1145/3167090},
year = {2018},
}
Publisher's Version
Article: poplws18cppmain-id14-p doi:10.1145/3167090
|
| |
Ringer, Talia |
CPP '18: "Adapting Proof Automation ..."
Adapting Proof Automation to Adapt Proofs
Talia Ringer, Nathaniel Yazdani, John Leo, and Dan Grossman
(University of Washington, USA; Halfaya Research, USA)
@InProceedings{CPP18p161,
author = {Talia Ringer and Nathaniel Yazdani and John Leo and Dan Grossman},
title = {Adapting Proof Automation to Adapt Proofs},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {161-160},
doi = {10.1145/3167094},
year = {2018},
}
Publisher's Version
Article: poplws18cppmain-id23-p doi:10.1145/3167094
|
| |
Rizkallah, Christine |
CPP '18: "Total Haskell is Reasonable ..."
Total Haskell is Reasonable Coq
Antal Spector-Zabusky, Joachim Breitner, Christine Rizkallah, and Stephanie Weirich
(University of Pennsylvania, USA)
@InProceedings{CPP18p33,
author = {Antal Spector-Zabusky and Joachim Breitner and Christine Rizkallah and Stephanie Weirich},
title = {Total Haskell is Reasonable Coq},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {33-32},
doi = {10.1145/3167092},
year = {2018},
}
Publisher's Version
Article: poplws18cppmain-id51-p doi:10.1145/3167092
|
| |
Rouhling, Damien |
CPP '18: "A Formal Proof in Coq of a ..."
A Formal Proof in Coq of a Control Function for the Inverted Pendulum
Damien Rouhling
(University of Côte d'Azur, France; Inria, France)
@InProceedings{CPP18p49,
author = {Damien Rouhling},
title = {A Formal Proof in Coq of a Control Function for the Inverted Pendulum},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {49-48},
doi = {10.1145/3167101},
year = {2018},
}
Publisher's Version
Article: poplws18cppmain-id41-p doi:10.1145/3167101
|
| |
Schäfer, Steven
|
CPP '18: "Binder Aware Recursion over ..."
Binder Aware Recursion over Well-Scoped de Bruijn Syntax
Jonas Kaiser, Steven Schäfer, and Kathrin Stark
(Saarland University, Germany)
@InProceedings{CPP18p369,
author = {Jonas Kaiser and Steven Schäfer and Kathrin Stark},
title = {Binder Aware Recursion over Well-Scoped de Bruijn Syntax},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {369-368},
doi = {10.1145/3167098},
year = {2018},
}
Publisher's Version
Article: poplws18cppmain-id60-p doi:10.1145/3167098
|
| |
Schmitt, Alan |
CPP '18: "HOπ in Coq ..."
HOπ in Coq
Sergueï Lenglet and Alan Schmitt
(University of Lorraine, France; Inria, France)
@InProceedings{CPP18p321,
author = {Sergueï Lenglet and Alan Schmitt},
title = {HOπ in Coq},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {321-320},
doi = {10.1145/3167083},
year = {2018},
}
Publisher's Version
Article: poplws18cppmain-id18-p doi:10.1145/3167083
|
| |
Sergey, Ilya |
CPP '18: "Mechanising Blockchain Consensus ..."
Mechanising Blockchain Consensus
George Pîrlea and Ilya Sergey
(University College London, UK)
@InProceedings{CPP18p113,
author = {George Pîrlea and Ilya Sergey},
title = {Mechanising Blockchain Consensus},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {113-112},
doi = {10.1145/3167086},
year = {2018},
}
Publisher's Version
Article: poplws18cppmain-id48-p doi:10.1145/3167086
|
| |
Shankar, Natarajan |
CPP '18: "Proofs in Conflict-Driven ..."
Proofs in Conflict-Driven Theory Combination
Maria Paola Bonacina, Stéphane Graham-Lengrand, and Natarajan Shankar
(University of Verona, Italy; CNRS, France; Inria, France; École Polytechnique, France; SRI International, USA)
@InProceedings{CPP18p241,
author = {Maria Paola Bonacina and Stéphane Graham-Lengrand and Natarajan Shankar},
title = {Proofs in Conflict-Driven Theory Combination},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {241-240},
doi = {10.1145/3167096},
year = {2018},
}
Publisher's Version
Article: poplws18cppmain-id32-p doi:10.1145/3167096
|
| |
Smolka, Gert |
CPP '18: "Large Model Constructions ..."
Large Model Constructions for Second-Order ZF in Dependent Type Theory
Dominik Kirst and Gert Smolka
(Saarland University, Germany)
@InProceedings{CPP18p289,
author = {Dominik Kirst and Gert Smolka},
title = {Large Model Constructions for Second-Order ZF in Dependent Type Theory},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {289-288},
doi = {10.1145/3167095},
year = {2018},
}
Publisher's Version
Article: poplws18cppmain-id8-p doi:10.1145/3167095
|
| |
Spector-Zabusky, Antal |
CPP '18: "Total Haskell is Reasonable ..."
Total Haskell is Reasonable Coq
Antal Spector-Zabusky, Joachim Breitner, Christine Rizkallah, and Stephanie Weirich
(University of Pennsylvania, USA)
@InProceedings{CPP18p33,
author = {Antal Spector-Zabusky and Joachim Breitner and Christine Rizkallah and Stephanie Weirich},
title = {Total Haskell is Reasonable Coq},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {33-32},
doi = {10.1145/3167092},
year = {2018},
}
Publisher's Version
Article: poplws18cppmain-id51-p doi:10.1145/3167092
|
| |
Staples, Mark |
CPP '18: "Towards Verifying Ethereum ..."
Towards Verifying Ethereum Smart Contract Bytecode in Isabelle/HOL
Sidney Amani, Myriam Bégel, Maksym Bortin, and Mark Staples
(Data61 at CSIRO, Australia; ENS Paris-Saclay, France; University of Paris-Saclay, France; UNSW, Australia)
@InProceedings{CPP18p97,
author = {Sidney Amani and Myriam Bégel and Maksym Bortin and Mark Staples},
title = {Towards Verifying Ethereum Smart Contract Bytecode in Isabelle/HOL},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {97-96},
doi = {10.1145/3167084},
year = {2018},
}
Publisher's Version
Article: poplws18cppmain-id25-p doi:10.1145/3167084
|
| |
Stark, Ian |
CPP '18: "Triangulating Context Lemmas ..."
Triangulating Context Lemmas
Craig McLaughlin, James McKinna, and Ian Stark
(University of Edinburgh, UK)
@InProceedings{CPP18p145,
author = {Craig McLaughlin and James McKinna and Ian Stark},
title = {Triangulating Context Lemmas},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {145-144},
doi = {10.1145/3167081},
year = {2018},
}
Publisher's Version
Article: poplws18cppmain-id2-p doi:10.1145/3167081
|
| |
Stark, Kathrin |
CPP '18: "Binder Aware Recursion over ..."
Binder Aware Recursion over Well-Scoped de Bruijn Syntax
Jonas Kaiser, Steven Schäfer, and Kathrin Stark
(Saarland University, Germany)
@InProceedings{CPP18p369,
author = {Jonas Kaiser and Steven Schäfer and Kathrin Stark},
title = {Binder Aware Recursion over Well-Scoped de Bruijn Syntax},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {369-368},
doi = {10.1145/3167098},
year = {2018},
}
Publisher's Version
Article: poplws18cppmain-id60-p doi:10.1145/3167098
|
| |
Stump, Aaron |
CPP '18: "Generic Derivation of Induction ..."
Generic Derivation of Induction for Impredicative Encodings in Cedille
Denis Firsov and Aaron Stump
(University of Iowa, USA)
@InProceedings{CPP18p273,
author = {Denis Firsov and Aaron Stump},
title = {Generic Derivation of Induction for Impredicative Encodings in Cedille},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {273-272},
doi = {10.1145/3167087},
year = {2018},
}
Publisher's Version
Article: poplws18cppmain-id49-p doi:10.1145/3167087
|
| |
Swamy, Nikhil |
CPP '18: "A Monadic Framework for Relational ..."
A Monadic Framework for Relational Verification: Applied to Information Security, Program Equivalence, and Optimizations
Niklas Grimm, Kenji Maillard, Cédric Fournet, Cătălin Hriţcu, Matteo Maffei, Jonathan Protzenko, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy, and Santiago Zanella-Béguelin
(Vienna University of Technology, Austria; Inria, France; ENS Paris, France; Microsoft Research, UK; Microsoft Research, USA; Microsoft Research, India)
@InProceedings{CPP18p177,
author = {Niklas Grimm and Kenji Maillard and Cédric Fournet and Cătălin Hriţcu and Matteo Maffei and Jonathan Protzenko and Tahina Ramananandro and Aseem Rastogi and Nikhil Swamy and Santiago Zanella-Béguelin},
title = {A Monadic Framework for Relational Verification: Applied to Information Security, Program Equivalence, and Optimizations},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {177-176},
doi = {10.1145/3167090},
year = {2018},
}
Publisher's Version
Article: poplws18cppmain-id14-p doi:10.1145/3167090
|
| |
Tatlock, Zachary
|
CPP '18: "Œuf: Minimizing the Coq Extraction ..."
Œuf: Minimizing the Coq Extraction TCB
Eric Mullen, Stuart Pernsteiner, James R. Wilcox, Zachary Tatlock, and Dan Grossman
(University of Washington, USA)
@InProceedings{CPP18p225,
author = {Eric Mullen and Stuart Pernsteiner and James R. Wilcox and Zachary Tatlock and Dan Grossman},
title = {Œuf: Minimizing the Coq Extraction TCB},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {225-224},
doi = {10.1145/3167089},
year = {2018},
}
Publisher's Version
Article: poplws18cppmain-id12-p doi:10.1145/3167089
|
| |
Thiemann, René |
CPP '18: "Efficient Certification of ..."
Efficient Certification of Complexity Proofs: Formalizing the Perron–Frobenius Theorem (Invited Talk Paper)
Jose Divasón, Sebastiaan Joosten, Ondřej Kunčar, René Thiemann, and Akihisa Yamada
(University of La Rioja, Spain; University of Twente, Netherlands; TU Munich, Germany; University of Innsbruck, Austria; National Institute of Informatics, Japan)
@InProceedings{CPP18p17,
author = {Jose Divasón and Sebastiaan Joosten and Ondřej Kunčar and René Thiemann and Akihisa Yamada},
title = {Efficient Certification of Complexity Proofs: Formalizing the Perron–Frobenius Theorem (Invited Talk Paper)},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {17-16},
doi = {},
year = {2018},
}
Article: poplws18cppmain-id101-p doi:
|
| |
Watt, Conrad
|
CPP '18: "Mechanising and Verifying ..."
Mechanising and Verifying the WebAssembly Specification
Conrad Watt
(University of Cambridge, UK)
@InProceedings{CPP18p81,
author = {Conrad Watt},
title = {Mechanising and Verifying the WebAssembly Specification},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {81-80},
doi = {10.1145/3167082},
year = {2018},
}
Publisher's Version
Article: poplws18cppmain-id13-p doi:10.1145/3167082
|
| |
Weide, Niels van der |
CPP '18: "Finite Sets in Homotopy Type ..."
Finite Sets in Homotopy Type Theory
Dan Frumin, Herman Geuvers, Léon Gondelman, and Niels van der Weide
(Radboud University Nijmegen, Netherlands)
@InProceedings{CPP18p257,
author = {Dan Frumin and Herman Geuvers and Léon Gondelman and Niels van der Weide},
title = {Finite Sets in Homotopy Type Theory},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {257-256},
doi = {10.1145/3167085},
year = {2018},
}
Publisher's Version
Article: poplws18cppmain-id38-p doi:10.1145/3167085
|
| |
Weirich, Stephanie |
CPP '18: "Total Haskell is Reasonable ..."
Total Haskell is Reasonable Coq
Antal Spector-Zabusky, Joachim Breitner, Christine Rizkallah, and Stephanie Weirich
(University of Pennsylvania, USA)
@InProceedings{CPP18p33,
author = {Antal Spector-Zabusky and Joachim Breitner and Christine Rizkallah and Stephanie Weirich},
title = {Total Haskell is Reasonable Coq},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {33-32},
doi = {10.1145/3167092},
year = {2018},
}
Publisher's Version
Article: poplws18cppmain-id51-p doi:10.1145/3167092
|
| |
Wieczorek, Paweł |
CPP '18: "A Coq Formalization of Normalization ..."
A Coq Formalization of Normalization by Evaluation for Martin-Löf Type Theory
Paweł Wieczorek and Dariusz Biernacki
(University of Wrocław, Poland)
@InProceedings{CPP18p337,
author = {Paweł Wieczorek and Dariusz Biernacki},
title = {A Coq Formalization of Normalization by Evaluation for Martin-Löf Type Theory},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {337-336},
doi = {10.1145/3167091},
year = {2018},
}
Publisher's Version
Article: poplws18cppmain-id37-p doi:10.1145/3167091
|
| |
Wilcox, James R. |
CPP '18: "Œuf: Minimizing the Coq Extraction ..."
Œuf: Minimizing the Coq Extraction TCB
Eric Mullen, Stuart Pernsteiner, James R. Wilcox, Zachary Tatlock, and Dan Grossman
(University of Washington, USA)
@InProceedings{CPP18p225,
author = {Eric Mullen and Stuart Pernsteiner and James R. Wilcox and Zachary Tatlock and Dan Grossman},
title = {Œuf: Minimizing the Coq Extraction TCB},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {225-224},
doi = {10.1145/3167089},
year = {2018},
}
Publisher's Version
Article: poplws18cppmain-id12-p doi:10.1145/3167089
|
| |
Yamada, Akihisa
|
CPP '18: "Efficient Certification of ..."
Efficient Certification of Complexity Proofs: Formalizing the Perron–Frobenius Theorem (Invited Talk Paper)
Jose Divasón, Sebastiaan Joosten, Ondřej Kunčar, René Thiemann, and Akihisa Yamada
(University of La Rioja, Spain; University of Twente, Netherlands; TU Munich, Germany; University of Innsbruck, Austria; National Institute of Informatics, Japan)
@InProceedings{CPP18p17,
author = {Jose Divasón and Sebastiaan Joosten and Ondřej Kunčar and René Thiemann and Akihisa Yamada},
title = {Efficient Certification of Complexity Proofs: Formalizing the Perron–Frobenius Theorem (Invited Talk Paper)},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {17-16},
doi = {},
year = {2018},
}
Article: poplws18cppmain-id101-p doi:
|
| |
Yazdani, Nathaniel |
CPP '18: "Adapting Proof Automation ..."
Adapting Proof Automation to Adapt Proofs
Talia Ringer, Nathaniel Yazdani, John Leo, and Dan Grossman
(University of Washington, USA; Halfaya Research, USA)
@InProceedings{CPP18p161,
author = {Talia Ringer and Nathaniel Yazdani and John Leo and Dan Grossman},
title = {Adapting Proof Automation to Adapt Proofs},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {161-160},
doi = {10.1145/3167094},
year = {2018},
}
Publisher's Version
Article: poplws18cppmain-id23-p doi:10.1145/3167094
|
| |
Zanella-Béguelin, Santiago
|
CPP '18: "A Monadic Framework for Relational ..."
A Monadic Framework for Relational Verification: Applied to Information Security, Program Equivalence, and Optimizations
Niklas Grimm, Kenji Maillard, Cédric Fournet, Cătălin Hriţcu, Matteo Maffei, Jonathan Protzenko, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy, and Santiago Zanella-Béguelin
(Vienna University of Technology, Austria; Inria, France; ENS Paris, France; Microsoft Research, UK; Microsoft Research, USA; Microsoft Research, India)
@InProceedings{CPP18p177,
author = {Niklas Grimm and Kenji Maillard and Cédric Fournet and Cătălin Hriţcu and Matteo Maffei and Jonathan Protzenko and Tahina Ramananandro and Aseem Rastogi and Nikhil Swamy and Santiago Zanella-Béguelin},
title = {A Monadic Framework for Relational Verification: Applied to Information Security, Program Equivalence, and Optimizations},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {177-176},
doi = {10.1145/3167090},
year = {2018},
}
Publisher's Version
Article: poplws18cppmain-id14-p doi:10.1145/3167090
|