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 = {},
year = {2018},
}
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 = {},
year = {2018},
}
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 = {},
year = {2018},
}
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 = {},
year = {2018},
}
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 = {},
year = {2018},
}
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 = {},
year = {2018},
}
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 = {},
year = {2018},
}
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 = {},
year = {2018},
}
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 = {},
year = {2018},
}
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},
}
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 = {},
year = {2018},
}
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 = {},
year = {2018},
}
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 = {},
year = {2018},
}
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 = {},
year = {2018},
}
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 = {},
year = {2018},
}
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 = {},
year = {2018},
}
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 = {},
year = {2018},
}
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 = {},
year = {2018},
}
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 = {},
year = {2018},
}
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 = {},
year = {2018},
}
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 = {},
year = {2018},
}
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 = {},
year = {2018},
}
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 = {},
year = {2018},
}
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 = {},
year = {2018},
}
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 = {},
year = {2018},
}
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},
}
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 = {},
year = {2018},
}
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 = {},
year = {2018},
}
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 = {},
year = {2018},
}
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},
}
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 = {},
year = {2018},
}
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 = {},
year = {2018},
}
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 = {},
year = {2018},
}
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 = {},
year = {2018},
}
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 = {},
year = {2018},
}
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 = {},
year = {2018},
}
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 = {},
year = {2018},
}
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 = {},
year = {2018},
}
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 = {},
year = {2018},
}
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 = {},
year = {2018},
}
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 = {},
year = {2018},
}
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 = {},
year = {2018},
}
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 = {},
year = {2018},
}
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 = {},
year = {2018},
}
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 = {},
year = {2018},
}
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 = {},
year = {2018},
}
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 = {},
year = {2018},
}
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 = {},
year = {2018},
}
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 = {},
year = {2018},
}
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 = {},
year = {2018},
}
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 = {},
year = {2018},
}
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 = {},
year = {2018},
}
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 = {},
year = {2018},
}
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 = {},
year = {2018},
}
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 = {},
year = {2018},
}
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 = {},
year = {2018},
}
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 = {},
year = {2018},
}
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 = {},
year = {2018},
}
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 = {},
year = {2018},
}
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 = {},
year = {2018},
}
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 = {},
year = {2018},
}
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 = {},
year = {2018},
}
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 = {},
year = {2018},
}
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},
}
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 = {},
year = {2018},
}
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 = {},
year = {2018},
}
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 = {},
year = {2018},
}
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 = {},
year = {2018},
}
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 = {},
year = {2018},
}
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},
}
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 = {},
year = {2018},
}
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 = {},
year = {2018},
}