| |
Altmanninger, Johannes
|
CPP '20: "Frying the Egg, Roasting the ..."
Frying the Egg, Roasting the Chicken: Unit Deletions in DRAT Proofs
Johannes Altmanninger and Adrián Rebola Pardo
(TU Vienna, Austria)
@InProceedings{CPP20p109,
author = {Johannes Altmanninger and Adrián Rebola Pardo},
title = {Frying the Egg, Roasting the Chicken: Unit Deletions in DRAT Proofs},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {109-108},
doi = {10.1145/3372885.3373821},
year = {2020},
}
 Publisher's Version
Article: poplws20cppmain-p21-p doi:10.1145/3372885.3373821
|
| |
Annenkov, Danil |
CPP '20: "ConCert: A Smart Contract ..."
ConCert: A Smart Contract Certification Framework in Coq
Danil Annenkov, Jakob Botsch Nielsen, and Bas Spitters
(Aarhus University, Denmark)
@InProceedings{CPP20p307,
author = {Danil Annenkov and Jakob Botsch Nielsen and Bas Spitters},
title = {ConCert: A Smart Contract Certification Framework in Coq},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {307-306},
doi = {10.1145/3372885.3373829},
year = {2020},
}
Publisher's Version
 Published Artifact
Artifacts Available
Article: poplws20cppmain-p50-p doi:10.1145/3372885.3373829
|
| |
Aspinall, David |
CPP '20: "Formalising Oblivious Transfer ..."
Formalising Oblivious Transfer in the Semi-honest and Malicious Model in CryptHOL
David Butler, David Aspinall, and Adrià Gascón
(Alan Turing Institute, UK; University of Edinburgh, UK; Google, UK)
@InProceedings{CPP20p325,
author = {David Butler and David Aspinall and Adrià Gascón},
title = {Formalising Oblivious Transfer in the Semi-honest and Malicious Model in CryptHOL},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {325-324},
doi = {10.1145/3372885.3373815},
year = {2020},
}
Publisher's Version
Article: poplws20cppmain-p48-p doi:10.1145/3372885.3373815
|
| |
Bach Poulsen, Casper
|
CPP '20: "Intrinsically-Typed Definitional ..."
Intrinsically-Typed Definitional Interpreters for Linear, Session-Typed Languages
Arjen Rouvoet, Casper Bach Poulsen, Robbert Krebbers, and Eelco Visser
(Delft University of Technology, Netherlands)
@InProceedings{CPP20p397,
author = {Arjen Rouvoet and Casper Bach Poulsen and Robbert Krebbers and Eelco Visser},
title = {Intrinsically-Typed Definitional Interpreters for Linear, Session-Typed Languages},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {397-396},
doi = {10.1145/3372885.3373818},
year = {2020},
}
Publisher's Version
Published Artifact
Artifacts Available
Article: poplws20cppmain-p83-p doi:10.1145/3372885.3373818
|
| |
Blaudeau, Clement |
CPP '20: "A Verified Packrat Parser ..."
A Verified Packrat Parser Interpreter for Parsing Expression Grammars
Clement Blaudeau and Natarajan Shankar
(École Polytechnique, France; SRI International, USA)
@InProceedings{CPP20p37,
author = {Clement Blaudeau and Natarajan Shankar},
title = {A Verified Packrat Parser Interpreter for Parsing Expression Grammars},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {37-36},
doi = {10.1145/3372885.3373836},
year = {2020},
}
Publisher's Version
Article: poplws20cppmain-p77-p doi:10.1145/3372885.3373836
|
| |
Brown, Chad |
CPP '20: "Exploration of Neural Machine ..."
Exploration of Neural Machine Translation in Autoformalization of Mathematics in Mizar
Qingxiang Wang, Chad Brown, Cezary Kaliszyk, and Josef Urban
(University of Innsbruck, Austria; Czech Technical University in Prague, Czechia; University of Warsaw, Poland)
@InProceedings{CPP20p145,
author = {Qingxiang Wang and Chad Brown and Cezary Kaliszyk and Josef Urban},
title = {Exploration of Neural Machine Translation in Autoformalization of Mathematics in Mizar},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {145-144},
doi = {10.1145/3372885.3373827},
year = {2020},
}
Publisher's Version
Article: poplws20cppmain-p47-p doi:10.1145/3372885.3373827
|
| |
Buldas, Ahto |
CPP '20: "Verified Security of BLT Signature ..."
Verified Security of BLT Signature Scheme
Denis Firsov, Ahto Buldas, Ahto Truu, and Risto Laanoja
(Tallinn University of Technology, Estonia; Guardtime, Estonia)
@InProceedings{CPP20p343,
author = {Denis Firsov and Ahto Buldas and Ahto Truu and Risto Laanoja},
title = {Verified Security of BLT Signature Scheme},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {343-342},
doi = {10.1145/3372885.3373828},
year = {2020},
}
Publisher's Version
Article: poplws20cppmain-p49-p doi:10.1145/3372885.3373828
|
| |
Butler, David |
CPP '20: "Formalising Oblivious Transfer ..."
Formalising Oblivious Transfer in the Semi-honest and Malicious Model in CryptHOL
David Butler, David Aspinall, and Adrià Gascón
(Alan Turing Institute, UK; University of Edinburgh, UK; Google, UK)
@InProceedings{CPP20p325,
author = {David Butler and David Aspinall and Adrià Gascón},
title = {Formalising Oblivious Transfer in the Semi-honest and Malicious Model in CryptHOL},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {325-324},
doi = {10.1145/3372885.3373815},
year = {2020},
}
Publisher's Version
Article: poplws20cppmain-p48-p doi:10.1145/3372885.3373815
|
| |
Buzzard, Kevin |
CPP '20: "Formalising Perfectoid Spaces ..."
Formalising Perfectoid Spaces
Kevin Buzzard, Johan Commelin, and Patrick Massot
(Imperial College London, UK; University of Freiburg, Germany; University of Paris-Sud, France; CNRS, France)
@InProceedings{CPP20p415,
author = {Kevin Buzzard and Johan Commelin and Patrick Massot},
title = {Formalising Perfectoid Spaces},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {415-414},
doi = {10.1145/3372885.3373830},
year = {2020},
}
Publisher's Version
Article: poplws20cppmain-p59-p doi:10.1145/3372885.3373830
|
| |
Chen, Xiaohong
|
CPP '20: "Matching Logic: The Foundation ..."
Matching Logic: The Foundation of the K Framework (Invited Talk)
Grigore Roşu and Xiaohong Chen
(University of Illinois at Urbana-Champaign, USA; Runtime Verification, USA)
@InProceedings{CPP20p1,
author = {Grigore Roşu and Xiaohong Chen},
title = {Matching Logic: The Foundation of the K Framework (Invited Talk)},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {1-0},
doi = {10.1145/3372885.3378574},
year = {2020},
}
Publisher's Version
Article: poplws20cppmain-k2-p doi:10.1145/3372885.3378574
|
| |
Chlipala, Adam |
CPP '20: "Proof Assistants at the Hardware-Software ..."
Proof Assistants at the Hardware-Software Interface (Invited Talk)
Adam Chlipala
(Massachusetts Institute of Technology, USA)
@InProceedings{CPP20p19,
author = {Adam Chlipala},
title = {Proof Assistants at the Hardware-Software Interface (Invited Talk)},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {19-18},
doi = {10.1145/3372885.3378575},
year = {2020},
}
Publisher's Version
Article: poplws20cppmain-k1-p doi:10.1145/3372885.3378575
|
| |
Commelin, Johan |
CPP '20: "Formalising Perfectoid Spaces ..."
Formalising Perfectoid Spaces
Kevin Buzzard, Johan Commelin, and Patrick Massot
(Imperial College London, UK; University of Freiburg, Germany; University of Paris-Sud, France; CNRS, France)
@InProceedings{CPP20p415,
author = {Kevin Buzzard and Johan Commelin and Patrick Massot},
title = {Formalising Perfectoid Spaces},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {415-414},
doi = {10.1145/3372885.3373830},
year = {2020},
}
Publisher's Version
Article: poplws20cppmain-p59-p doi:10.1145/3372885.3373830
|
| |
Díaz, Tomás
|
CPP '20: "A Mechanized Formalization ..."
A Mechanized Formalization of GraphQL
Tomás Díaz, Federico Olmedo, and Éric Tanter
(IMFD, Chile; University of Chile, Chile; Inria, France)
@InProceedings{CPP20p289,
author = {Tomás Díaz and Federico Olmedo and Éric Tanter},
title = {A Mechanized Formalization of GraphQL},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {289-288},
doi = {10.1145/3372885.3373822},
year = {2020},
}
Publisher's Version
Article: poplws20cppmain-p22-p doi:10.1145/3372885.3373822
|
| |
Doczkal, Christian |
CPP '20: "Completeness of an Axiomatization ..."
Completeness of an Axiomatization of Graph Isomorphism via Graph Rewriting in Coq
Christian Doczkal and Damien Pous
(University of Côte d'Azur, France; Inria, France; University of Lyon, France; CNRS, France; ENS Lyon, France)
@InProceedings{CPP20p451,
author = {Christian Doczkal and Damien Pous},
title = {Completeness of an Axiomatization of Graph Isomorphism via Graph Rewriting in Coq},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {451-450},
doi = {10.1145/3372885.3373831},
year = {2020},
}
Publisher's Version
Published Artifact
Artifacts Available
Article: poplws20cppmain-p60-p doi:10.1145/3372885.3373831
|
| |
Firsov, Denis
|
CPP '20: "Verified Security of BLT Signature ..."
Verified Security of BLT Signature Scheme
Denis Firsov, Ahto Buldas, Ahto Truu, and Risto Laanoja
(Tallinn University of Technology, Estonia; Guardtime, Estonia)
@InProceedings{CPP20p343,
author = {Denis Firsov and Ahto Buldas and Ahto Truu and Risto Laanoja},
title = {Verified Security of BLT Signature Scheme},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {343-342},
doi = {10.1145/3372885.3373828},
year = {2020},
}
Publisher's Version
Article: poplws20cppmain-p49-p doi:10.1145/3372885.3373828
|
| |
Forsberg, Fredrik Nordvall |
CPP '20: "Three Equivalent Ordinal Notation ..."
Three Equivalent Ordinal Notation Systems in Cubical Agda
Fredrik Nordvall Forsberg, Chuangjie Xu, and Neil Ghani
(University of Strathclyde, UK; LMU Munich, Germany)
@InProceedings{CPP20p253,
author = {Fredrik Nordvall Forsberg and Chuangjie Xu and Neil Ghani},
title = {Three Equivalent Ordinal Notation Systems in Cubical Agda},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {253-252},
doi = {10.1145/3372885.3373835},
year = {2020},
}
Publisher's Version
Published Artifact
Artifacts Available
Article: poplws20cppmain-p74-p doi:10.1145/3372885.3373835
|
| |
Forster, Yannick |
CPP '20: "Verified Programming of Turing ..."
Verified Programming of Turing Machines in Coq
Yannick Forster, Fabian Kunze, and Maximilian Wuttke
(Saarland University, Germany)
@InProceedings{CPP20p181,
author = {Yannick Forster and Fabian Kunze and Maximilian Wuttke},
title = {Verified Programming of Turing Machines in Coq},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {181-180},
doi = {10.1145/3372885.3373816},
year = {2020},
}
Publisher's Version
Article: poplws20cppmain-p63-p doi:10.1145/3372885.3373816
CPP '20: "Undecidability of Higher-Order ..."
Undecidability of Higher-Order Unification Formalised in Coq
Simon Spies and Yannick Forster
(Saarland University, Germany)
@InProceedings{CPP20p217,
author = {Simon Spies and Yannick Forster},
title = {Undecidability of Higher-Order Unification Formalised in Coq},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {217-216},
doi = {10.1145/3372885.3373832},
year = {2020},
}
Publisher's Version
Article: poplws20cppmain-p62-p doi:10.1145/3372885.3373832
CPP '20: "Coq à la Carte: A Practical ..."
Coq à la Carte: A Practical Approach to Modular Syntax with Binders
Yannick Forster and Kathrin Stark
(Saarland University, Germany)
@InProceedings{CPP20p271,
author = {Yannick Forster and Kathrin Stark},
title = {Coq à la Carte: A Practical Approach to Modular Syntax with Binders},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {271-270},
doi = {10.1145/3372885.3373817},
year = {2020},
}
Publisher's Version
Article: poplws20cppmain-p64-p doi:10.1145/3372885.3373817
|
| |
Gascón, Adrià
|
CPP '20: "Formalising Oblivious Transfer ..."
Formalising Oblivious Transfer in the Semi-honest and Malicious Model in CryptHOL
David Butler, David Aspinall, and Adrià Gascón
(Alan Turing Institute, UK; University of Edinburgh, UK; Google, UK)
@InProceedings{CPP20p325,
author = {David Butler and David Aspinall and Adrià Gascón},
title = {Formalising Oblivious Transfer in the Semi-honest and Malicious Model in CryptHOL},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {325-324},
doi = {10.1145/3372885.3373815},
year = {2020},
}
Publisher's Version
Article: poplws20cppmain-p48-p doi:10.1145/3372885.3373815
|
| |
Ghani, Neil |
CPP '20: "Three Equivalent Ordinal Notation ..."
Three Equivalent Ordinal Notation Systems in Cubical Agda
Fredrik Nordvall Forsberg, Chuangjie Xu, and Neil Ghani
(University of Strathclyde, UK; LMU Munich, Germany)
@InProceedings{CPP20p253,
author = {Fredrik Nordvall Forsberg and Chuangjie Xu and Neil Ghani},
title = {Three Equivalent Ordinal Notation Systems in Cubical Agda},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {253-252},
doi = {10.1145/3372885.3373835},
year = {2020},
}
Publisher's Version
Published Artifact
Artifacts Available
Article: poplws20cppmain-p74-p doi:10.1145/3372885.3373835
|
| |
Goel, Shilpi |
CPP '20: "Verifying x86 Instruction ..."
Verifying x86 Instruction Implementations
Shilpi Goel, Anna Slobodova, Rob Sumners, and Sol Swords
(Centaur Technology, USA)
@InProceedings{CPP20p91,
author = {Shilpi Goel and Anna Slobodova and Rob Sumners and Sol Swords},
title = {Verifying x86 Instruction Implementations},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {91-90},
doi = {10.1145/3372885.3373811},
year = {2020},
}
Publisher's Version
Article: poplws20cppmain-p38-p doi:10.1145/3372885.3373811
|
| |
Grossman, Dan |
CPP '20: "REPLica: REPL Instrumentation ..."
REPLica: REPL Instrumentation for Coq Analysis
Talia Ringer, Alex Sanchez-Stern, Dan Grossman, and Sorin Lerner
(University of Washington, USA; University of California at San Diego, USA)
@InProceedings{CPP20p163,
author = {Talia Ringer and Alex Sanchez-Stern and Dan Grossman and Sorin Lerner},
title = {REPLica: REPL Instrumentation for Coq Analysis},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {163-162},
doi = {10.1145/3372885.3373823},
year = {2020},
}
Publisher's Version
Article: poplws20cppmain-p27-p doi:10.1145/3372885.3373823
|
| |
Han, Jesse Michael
|
CPP '20: "A Formal Proof of the Independence ..."
A Formal Proof of the Independence of the Continuum Hypothesis
Jesse Michael Han and Floris van Doorn
(University of Pittsburgh, USA)
@InProceedings{CPP20p487,
author = {Jesse Michael Han and Floris van Doorn},
title = {A Formal Proof of the Independence of the Continuum Hypothesis},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {487-486},
doi = {10.1145/3372885.3373826},
year = {2020},
}
Publisher's Version
Article: poplws20cppmain-p36-p doi:10.1145/3372885.3373826
|
| |
He, Paul |
CPP '20: "An Equational Theory for Weak ..."
An Equational Theory for Weak Bisimulation via Generalized Parameterized Coinduction
Yannick Zakowski, Paul He, Chung-Kil Hur, and Steve Zdancewic
(University of Pennsylvania, USA; Seoul National University, South Korea)
@InProceedings{CPP20p127,
author = {Yannick Zakowski and Paul He and Chung-Kil Hur and Steve Zdancewic},
title = {An Equational Theory for Weak Bisimulation via Generalized Parameterized Coinduction},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {127-126},
doi = {10.1145/3372885.3373813},
year = {2020},
}
Publisher's Version
Article: poplws20cppmain-p44-p doi:10.1145/3372885.3373813
|
| |
Hobor, Aquinas |
CPP '20: "A Functional Proof Pearl: ..."
A Functional Proof Pearl: Inverting the Ackermann Hierarchy
Linh Tran, Anshuman Mohan, and Aquinas Hobor
(Yale University, USA; National University of Singapore, Singapore)
@InProceedings{CPP20p199,
author = {Linh Tran and Anshuman Mohan and Aquinas Hobor},
title = {A Functional Proof Pearl: Inverting the Ackermann Hierarchy},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {199-198},
doi = {10.1145/3372885.3373837},
year = {2020},
}
Publisher's Version
Article: poplws20cppmain-p87-p doi:10.1145/3372885.3373837
|
| |
Hur, Chung-Kil |
CPP '20: "An Equational Theory for Weak ..."
An Equational Theory for Weak Bisimulation via Generalized Parameterized Coinduction
Yannick Zakowski, Paul He, Chung-Kil Hur, and Steve Zdancewic
(University of Pennsylvania, USA; Seoul National University, South Korea)
@InProceedings{CPP20p127,
author = {Yannick Zakowski and Paul He and Chung-Kil Hur and Steve Zdancewic},
title = {An Equational Theory for Weak Bisimulation via Generalized Parameterized Coinduction},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {127-126},
doi = {10.1145/3372885.3373813},
year = {2020},
}
Publisher's Version
Article: poplws20cppmain-p44-p doi:10.1145/3372885.3373813
|
| |
Immler, Fabian
|
CPP '20: "The Poincaré-Bendixson Theorem ..."
The Poincaré-Bendixson Theorem in Isabelle/HOL
Fabian Immler and Yong Kiam Tan
(Carnegie Mellon University, USA)
@InProceedings{CPP20p469,
author = {Fabian Immler and Yong Kiam Tan},
title = {The Poincaré-Bendixson Theorem in Isabelle/HOL},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {469-468},
doi = {10.1145/3372885.3373833},
year = {2020},
}
Publisher's Version
Article: poplws20cppmain-p68-p doi:10.1145/3372885.3373833
|
| |
Kaliszyk, Cezary
|
CPP '20: "Exploration of Neural Machine ..."
Exploration of Neural Machine Translation in Autoformalization of Mathematics in Mizar
Qingxiang Wang, Chad Brown, Cezary Kaliszyk, and Josef Urban
(University of Innsbruck, Austria; Czech Technical University in Prague, Czechia; University of Warsaw, Poland)
@InProceedings{CPP20p145,
author = {Qingxiang Wang and Chad Brown and Cezary Kaliszyk and Josef Urban},
title = {Exploration of Neural Machine Translation in Autoformalization of Mathematics in Mizar},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {145-144},
doi = {10.1145/3372885.3373827},
year = {2020},
}
Publisher's Version
Article: poplws20cppmain-p47-p doi:10.1145/3372885.3373827
|
| |
Krebbers, Robbert |
CPP '20: "Intrinsically-Typed Definitional ..."
Intrinsically-Typed Definitional Interpreters for Linear, Session-Typed Languages
Arjen Rouvoet, Casper Bach Poulsen, Robbert Krebbers, and Eelco Visser
(Delft University of Technology, Netherlands)
@InProceedings{CPP20p397,
author = {Arjen Rouvoet and Casper Bach Poulsen and Robbert Krebbers and Eelco Visser},
title = {Intrinsically-Typed Definitional Interpreters for Linear, Session-Typed Languages},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {397-396},
doi = {10.1145/3372885.3373818},
year = {2020},
}
Publisher's Version
Published Artifact
Artifacts Available
Article: poplws20cppmain-p83-p doi:10.1145/3372885.3373818
|
| |
Kunze, Fabian |
CPP '20: "Verified Programming of Turing ..."
Verified Programming of Turing Machines in Coq
Yannick Forster, Fabian Kunze, and Maximilian Wuttke
(Saarland University, Germany)
@InProceedings{CPP20p181,
author = {Yannick Forster and Fabian Kunze and Maximilian Wuttke},
title = {Verified Programming of Turing Machines in Coq},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {181-180},
doi = {10.1145/3372885.3373816},
year = {2020},
}
Publisher's Version
Article: poplws20cppmain-p63-p doi:10.1145/3372885.3373816
|
| |
Laanoja, Risto
|
CPP '20: "Verified Security of BLT Signature ..."
Verified Security of BLT Signature Scheme
Denis Firsov, Ahto Buldas, Ahto Truu, and Risto Laanoja
(Tallinn University of Technology, Estonia; Guardtime, Estonia)
@InProceedings{CPP20p343,
author = {Denis Firsov and Ahto Buldas and Ahto Truu and Risto Laanoja},
title = {Verified Security of BLT Signature Scheme},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {343-342},
doi = {10.1145/3372885.3373828},
year = {2020},
}
Publisher's Version
Article: poplws20cppmain-p49-p doi:10.1145/3372885.3373828
|
| |
Lerner, Sorin |
CPP '20: "REPLica: REPL Instrumentation ..."
REPLica: REPL Instrumentation for Coq Analysis
Talia Ringer, Alex Sanchez-Stern, Dan Grossman, and Sorin Lerner
(University of Washington, USA; University of California at San Diego, USA)
@InProceedings{CPP20p163,
author = {Talia Ringer and Alex Sanchez-Stern and Dan Grossman and Sorin Lerner},
title = {REPLica: REPL Instrumentation for Coq Analysis},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {163-162},
doi = {10.1145/3372885.3373823},
year = {2020},
}
Publisher's Version
Article: poplws20cppmain-p27-p doi:10.1145/3372885.3373823
|
| |
Letan, Thomas |
CPP '20: "FreeSpec: Specifying, Verifying, ..."
FreeSpec: Specifying, Verifying, and Executing Impure Computations in Coq
Thomas Letan and Yann Régis-Gianas
(ANSSI, France; University of Paris, France; IRIF, France; Inria, France)
@InProceedings{CPP20p73,
author = {Thomas Letan and Yann Régis-Gianas},
title = {FreeSpec: Specifying, Verifying, and Executing Impure Computations in Coq},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {73-72},
doi = {10.1145/3372885.3373812},
year = {2020},
}
Publisher's Version
Article: poplws20cppmain-p42-p doi:10.1145/3372885.3373812
|
| |
Massot, Patrick
|
CPP '20: "Formalising Perfectoid Spaces ..."
Formalising Perfectoid Spaces
Kevin Buzzard, Johan Commelin, and Patrick Massot
(Imperial College London, UK; University of Freiburg, Germany; University of Paris-Sud, France; CNRS, France)
@InProceedings{CPP20p415,
author = {Kevin Buzzard and Johan Commelin and Patrick Massot},
title = {Formalising Perfectoid Spaces},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {415-414},
doi = {10.1145/3372885.3373830},
year = {2020},
}
Publisher's Version
Article: poplws20cppmain-p59-p doi:10.1145/3372885.3373830
|
| |
Mohan, Anshuman |
CPP '20: "A Functional Proof Pearl: ..."
A Functional Proof Pearl: Inverting the Ackermann Hierarchy
Linh Tran, Anshuman Mohan, and Aquinas Hobor
(Yale University, USA; National University of Singapore, Singapore)
@InProceedings{CPP20p199,
author = {Linh Tran and Anshuman Mohan and Aquinas Hobor},
title = {A Functional Proof Pearl: Inverting the Ackermann Hierarchy},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {199-198},
doi = {10.1145/3372885.3373837},
year = {2020},
}
Publisher's Version
Article: poplws20cppmain-p87-p doi:10.1145/3372885.3373837
|
| |
Mörtberg, Anders |
CPP '20: "Cubical Synthetic Homotopy ..."
Cubical Synthetic Homotopy Theory
Anders Mörtberg and Loïc Pujet
(Stockholm University, Sweden; Inria, France)
@InProceedings{CPP20p235,
author = {Anders Mörtberg and Loïc Pujet},
title = {Cubical Synthetic Homotopy Theory},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {235-234},
doi = {10.1145/3372885.3373825},
year = {2020},
}
Publisher's Version
Article: poplws20cppmain-p30-p doi:10.1145/3372885.3373825
|
| |
Natarajan, Raja
|
CPP '20: "A Constructive Formalization ..."
A Constructive Formalization of the Weak Perfect Graph Theorem
Abhishek Kr Singh and Raja Natarajan
(Tata Institute of Fundamental Research, India)
@InProceedings{CPP20p433,
author = {Abhishek Kr Singh and Raja Natarajan},
title = {A Constructive Formalization of the Weak Perfect Graph Theorem},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {433-432},
doi = {10.1145/3372885.3373819},
year = {2020},
}
Publisher's Version
Article: poplws20cppmain-p9-p doi:10.1145/3372885.3373819
|
| |
Nielsen, Jakob Botsch |
CPP '20: "ConCert: A Smart Contract ..."
ConCert: A Smart Contract Certification Framework in Coq
Danil Annenkov, Jakob Botsch Nielsen, and Bas Spitters
(Aarhus University, Denmark)
@InProceedings{CPP20p307,
author = {Danil Annenkov and Jakob Botsch Nielsen and Bas Spitters},
title = {ConCert: A Smart Contract Certification Framework in Coq},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {307-306},
doi = {10.1145/3372885.3373829},
year = {2020},
}
Publisher's Version
Published Artifact
Artifacts Available
Article: poplws20cppmain-p50-p doi:10.1145/3372885.3373829
|
| |
Nipkow, Tobias |
CPP '20: "Proof Pearl: Braun Trees ..."
Proof Pearl: Braun Trees
Tobias Nipkow and Thomas Sewell
(TU Munich, Germany; Chalmers University of Technology, Sweden)
@InProceedings{CPP20p55,
author = {Tobias Nipkow and Thomas Sewell},
title = {Proof Pearl: Braun Trees},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {55-54},
doi = {10.1145/3372885.3373834},
year = {2020},
}
Publisher's Version
Article: poplws20cppmain-p73-p doi:10.1145/3372885.3373834
|
| |
Olmedo, Federico
|
CPP '20: "A Mechanized Formalization ..."
A Mechanized Formalization of GraphQL
Tomás Díaz, Federico Olmedo, and Éric Tanter
(IMFD, Chile; University of Chile, Chile; Inria, France)
@InProceedings{CPP20p289,
author = {Tomás Díaz and Federico Olmedo and Éric Tanter},
title = {A Mechanized Formalization of GraphQL},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {289-288},
doi = {10.1145/3372885.3373822},
year = {2020},
}
Publisher's Version
Article: poplws20cppmain-p22-p doi:10.1145/3372885.3373822
|
| |
Overbeek, Roy |
CPP '20: "Formalizing Determinacy of ..."
Formalizing Determinacy of Concurrent Revisions
Roy Overbeek
(Vrije Universiteit Amsterdam, Netherlands)
@InProceedings{CPP20p361,
author = {Roy Overbeek},
title = {Formalizing Determinacy of Concurrent Revisions},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {361-360},
doi = {10.1145/3372885.3373820},
year = {2020},
}
Publisher's Version
Article: poplws20cppmain-p19-p doi:10.1145/3372885.3373820
|
| |
Pous, Damien
|
CPP '20: "Completeness of an Axiomatization ..."
Completeness of an Axiomatization of Graph Isomorphism via Graph Rewriting in Coq
Christian Doczkal and Damien Pous
(University of Côte d'Azur, France; Inria, France; University of Lyon, France; CNRS, France; ENS Lyon, France)
@InProceedings{CPP20p451,
author = {Christian Doczkal and Damien Pous},
title = {Completeness of an Axiomatization of Graph Isomorphism via Graph Rewriting in Coq},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {451-450},
doi = {10.1145/3372885.3373831},
year = {2020},
}
Publisher's Version
Published Artifact
Artifacts Available
Article: poplws20cppmain-p60-p doi:10.1145/3372885.3373831
|
| |
Pujet, Loïc |
CPP '20: "Cubical Synthetic Homotopy ..."
Cubical Synthetic Homotopy Theory
Anders Mörtberg and Loïc Pujet
(Stockholm University, Sweden; Inria, France)
@InProceedings{CPP20p235,
author = {Anders Mörtberg and Loïc Pujet},
title = {Cubical Synthetic Homotopy Theory},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {235-234},
doi = {10.1145/3372885.3373825},
year = {2020},
}
Publisher's Version
Article: poplws20cppmain-p30-p doi:10.1145/3372885.3373825
|
| |
Rebola Pardo, Adrián
|
CPP '20: "Frying the Egg, Roasting the ..."
Frying the Egg, Roasting the Chicken: Unit Deletions in DRAT Proofs
Johannes Altmanninger and Adrián Rebola Pardo
(TU Vienna, Austria)
@InProceedings{CPP20p109,
author = {Johannes Altmanninger and Adrián Rebola Pardo},
title = {Frying the Egg, Roasting the Chicken: Unit Deletions in DRAT Proofs},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {109-108},
doi = {10.1145/3372885.3373821},
year = {2020},
}
Publisher's Version
Article: poplws20cppmain-p21-p doi:10.1145/3372885.3373821
|
| |
Régis-Gianas, Yann |
CPP '20: "FreeSpec: Specifying, Verifying, ..."
FreeSpec: Specifying, Verifying, and Executing Impure Computations in Coq
Thomas Letan and Yann Régis-Gianas
(ANSSI, France; University of Paris, France; IRIF, France; Inria, France)
@InProceedings{CPP20p73,
author = {Thomas Letan and Yann Régis-Gianas},
title = {FreeSpec: Specifying, Verifying, and Executing Impure Computations in Coq},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {73-72},
doi = {10.1145/3372885.3373812},
year = {2020},
}
Publisher's Version
Article: poplws20cppmain-p42-p doi:10.1145/3372885.3373812
|
| |
Ringer, Talia |
CPP '20: "REPLica: REPL Instrumentation ..."
REPLica: REPL Instrumentation for Coq Analysis
Talia Ringer, Alex Sanchez-Stern, Dan Grossman, and Sorin Lerner
(University of Washington, USA; University of California at San Diego, USA)
@InProceedings{CPP20p163,
author = {Talia Ringer and Alex Sanchez-Stern and Dan Grossman and Sorin Lerner},
title = {REPLica: REPL Instrumentation for Coq Analysis},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {163-162},
doi = {10.1145/3372885.3373823},
year = {2020},
}
Publisher's Version
Article: poplws20cppmain-p27-p doi:10.1145/3372885.3373823
|
| |
Roşu, Grigore |
CPP '20: "Matching Logic: The Foundation ..."
Matching Logic: The Foundation of the K Framework (Invited Talk)
Grigore Roşu and Xiaohong Chen
(University of Illinois at Urbana-Champaign, USA; Runtime Verification, USA)
@InProceedings{CPP20p1,
author = {Grigore Roşu and Xiaohong Chen},
title = {Matching Logic: The Foundation of the K Framework (Invited Talk)},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {1-0},
doi = {10.1145/3372885.3378574},
year = {2020},
}
Publisher's Version
Article: poplws20cppmain-k2-p doi:10.1145/3372885.3378574
|
| |
Rouvoet, Arjen |
CPP '20: "Intrinsically-Typed Definitional ..."
Intrinsically-Typed Definitional Interpreters for Linear, Session-Typed Languages
Arjen Rouvoet, Casper Bach Poulsen, Robbert Krebbers, and Eelco Visser
(Delft University of Technology, Netherlands)
@InProceedings{CPP20p397,
author = {Arjen Rouvoet and Casper Bach Poulsen and Robbert Krebbers and Eelco Visser},
title = {Intrinsically-Typed Definitional Interpreters for Linear, Session-Typed Languages},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {397-396},
doi = {10.1145/3372885.3373818},
year = {2020},
}
Publisher's Version
Published Artifact
Artifacts Available
Article: poplws20cppmain-p83-p doi:10.1145/3372885.3373818
|
| |
Sanchez-Stern, Alex
|
CPP '20: "REPLica: REPL Instrumentation ..."
REPLica: REPL Instrumentation for Coq Analysis
Talia Ringer, Alex Sanchez-Stern, Dan Grossman, and Sorin Lerner
(University of Washington, USA; University of California at San Diego, USA)
@InProceedings{CPP20p163,
author = {Talia Ringer and Alex Sanchez-Stern and Dan Grossman and Sorin Lerner},
title = {REPLica: REPL Instrumentation for Coq Analysis},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {163-162},
doi = {10.1145/3372885.3373823},
year = {2020},
}
Publisher's Version
Article: poplws20cppmain-p27-p doi:10.1145/3372885.3373823
|
| |
Sewell, Thomas |
CPP '20: "Proof Pearl: Braun Trees ..."
Proof Pearl: Braun Trees
Tobias Nipkow and Thomas Sewell
(TU Munich, Germany; Chalmers University of Technology, Sweden)
@InProceedings{CPP20p55,
author = {Tobias Nipkow and Thomas Sewell},
title = {Proof Pearl: Braun Trees},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {55-54},
doi = {10.1145/3372885.3373834},
year = {2020},
}
Publisher's Version
Article: poplws20cppmain-p73-p doi:10.1145/3372885.3373834
|
| |
Shankar, Natarajan |
CPP '20: "A Verified Packrat Parser ..."
A Verified Packrat Parser Interpreter for Parsing Expression Grammars
Clement Blaudeau and Natarajan Shankar
(École Polytechnique, France; SRI International, USA)
@InProceedings{CPP20p37,
author = {Clement Blaudeau and Natarajan Shankar},
title = {A Verified Packrat Parser Interpreter for Parsing Expression Grammars},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {37-36},
doi = {10.1145/3372885.3373836},
year = {2020},
}
Publisher's Version
Article: poplws20cppmain-p77-p doi:10.1145/3372885.3373836
|
| |
Singh, Abhishek Kr |
CPP '20: "A Constructive Formalization ..."
A Constructive Formalization of the Weak Perfect Graph Theorem
Abhishek Kr Singh and Raja Natarajan
(Tata Institute of Fundamental Research, India)
@InProceedings{CPP20p433,
author = {Abhishek Kr Singh and Raja Natarajan},
title = {A Constructive Formalization of the Weak Perfect Graph Theorem},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {433-432},
doi = {10.1145/3372885.3373819},
year = {2020},
}
Publisher's Version
Article: poplws20cppmain-p9-p doi:10.1145/3372885.3373819
|
| |
Slobodova, Anna |
CPP '20: "Verifying x86 Instruction ..."
Verifying x86 Instruction Implementations
Shilpi Goel, Anna Slobodova, Rob Sumners, and Sol Swords
(Centaur Technology, USA)
@InProceedings{CPP20p91,
author = {Shilpi Goel and Anna Slobodova and Rob Sumners and Sol Swords},
title = {Verifying x86 Instruction Implementations},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {91-90},
doi = {10.1145/3372885.3373811},
year = {2020},
}
Publisher's Version
Article: poplws20cppmain-p38-p doi:10.1145/3372885.3373811
|
| |
Spies, Simon |
CPP '20: "Undecidability of Higher-Order ..."
Undecidability of Higher-Order Unification Formalised in Coq
Simon Spies and Yannick Forster
(Saarland University, Germany)
@InProceedings{CPP20p217,
author = {Simon Spies and Yannick Forster},
title = {Undecidability of Higher-Order Unification Formalised in Coq},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {217-216},
doi = {10.1145/3372885.3373832},
year = {2020},
}
Publisher's Version
Article: poplws20cppmain-p62-p doi:10.1145/3372885.3373832
|
| |
Spitters, Bas |
CPP '20: "ConCert: A Smart Contract ..."
ConCert: A Smart Contract Certification Framework in Coq
Danil Annenkov, Jakob Botsch Nielsen, and Bas Spitters
(Aarhus University, Denmark)
@InProceedings{CPP20p307,
author = {Danil Annenkov and Jakob Botsch Nielsen and Bas Spitters},
title = {ConCert: A Smart Contract Certification Framework in Coq},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {307-306},
doi = {10.1145/3372885.3373829},
year = {2020},
}
Publisher's Version
Published Artifact
Artifacts Available
Article: poplws20cppmain-p50-p doi:10.1145/3372885.3373829
|
| |
Stark, Kathrin |
CPP '20: "Coq à la Carte: A Practical ..."
Coq à la Carte: A Practical Approach to Modular Syntax with Binders
Yannick Forster and Kathrin Stark
(Saarland University, Germany)
@InProceedings{CPP20p271,
author = {Yannick Forster and Kathrin Stark},
title = {Coq à la Carte: A Practical Approach to Modular Syntax with Binders},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {271-270},
doi = {10.1145/3372885.3373817},
year = {2020},
}
Publisher's Version
Article: poplws20cppmain-p64-p doi:10.1145/3372885.3373817
|
| |
Sumners, Rob |
CPP '20: "Verifying x86 Instruction ..."
Verifying x86 Instruction Implementations
Shilpi Goel, Anna Slobodova, Rob Sumners, and Sol Swords
(Centaur Technology, USA)
@InProceedings{CPP20p91,
author = {Shilpi Goel and Anna Slobodova and Rob Sumners and Sol Swords},
title = {Verifying x86 Instruction Implementations},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {91-90},
doi = {10.1145/3372885.3373811},
year = {2020},
}
Publisher's Version
Article: poplws20cppmain-p38-p doi:10.1145/3372885.3373811
|
| |
Swords, Sol |
CPP '20: "Verifying x86 Instruction ..."
Verifying x86 Instruction Implementations
Shilpi Goel, Anna Slobodova, Rob Sumners, and Sol Swords
(Centaur Technology, USA)
@InProceedings{CPP20p91,
author = {Shilpi Goel and Anna Slobodova and Rob Sumners and Sol Swords},
title = {Verifying x86 Instruction Implementations},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {91-90},
doi = {10.1145/3372885.3373811},
year = {2020},
}
Publisher's Version
Article: poplws20cppmain-p38-p doi:10.1145/3372885.3373811
|
| |
Tan, Yong Kiam
|
CPP '20: "The Poincaré-Bendixson Theorem ..."
The Poincaré-Bendixson Theorem in Isabelle/HOL
Fabian Immler and Yong Kiam Tan
(Carnegie Mellon University, USA)
@InProceedings{CPP20p469,
author = {Fabian Immler and Yong Kiam Tan},
title = {The Poincaré-Bendixson Theorem in Isabelle/HOL},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {469-468},
doi = {10.1145/3372885.3373833},
year = {2020},
}
Publisher's Version
Article: poplws20cppmain-p68-p doi:10.1145/3372885.3373833
|
| |
Tanter, Éric |
CPP '20: "A Mechanized Formalization ..."
A Mechanized Formalization of GraphQL
Tomás Díaz, Federico Olmedo, and Éric Tanter
(IMFD, Chile; University of Chile, Chile; Inria, France)
@InProceedings{CPP20p289,
author = {Tomás Díaz and Federico Olmedo and Éric Tanter},
title = {A Mechanized Formalization of GraphQL},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {289-288},
doi = {10.1145/3372885.3373822},
year = {2020},
}
Publisher's Version
Article: poplws20cppmain-p22-p doi:10.1145/3372885.3373822
|
| |
The mathlib Community |
CPP '20: "The Lean Mathematical Library ..."
The Lean Mathematical Library
The mathlib Community
@InProceedings{CPP20p505,
author = { The mathlib Community},
title = {The Lean Mathematical Library},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {505-504},
doi = {10.1145/3372885.3373824},
year = {2020},
}
Publisher's Version
Article: poplws20cppmain-p29-p doi:10.1145/3372885.3373824
|
| |
Tran, Linh |
CPP '20: "A Functional Proof Pearl: ..."
A Functional Proof Pearl: Inverting the Ackermann Hierarchy
Linh Tran, Anshuman Mohan, and Aquinas Hobor
(Yale University, USA; National University of Singapore, Singapore)
@InProceedings{CPP20p199,
author = {Linh Tran and Anshuman Mohan and Aquinas Hobor},
title = {A Functional Proof Pearl: Inverting the Ackermann Hierarchy},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {199-198},
doi = {10.1145/3372885.3373837},
year = {2020},
}
Publisher's Version
Article: poplws20cppmain-p87-p doi:10.1145/3372885.3373837
|
| |
Truu, Ahto |
CPP '20: "Verified Security of BLT Signature ..."
Verified Security of BLT Signature Scheme
Denis Firsov, Ahto Buldas, Ahto Truu, and Risto Laanoja
(Tallinn University of Technology, Estonia; Guardtime, Estonia)
@InProceedings{CPP20p343,
author = {Denis Firsov and Ahto Buldas and Ahto Truu and Risto Laanoja},
title = {Verified Security of BLT Signature Scheme},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {343-342},
doi = {10.1145/3372885.3373828},
year = {2020},
}
Publisher's Version
Article: poplws20cppmain-p49-p doi:10.1145/3372885.3373828
|
| |
Urban, Josef
|
CPP '20: "Exploration of Neural Machine ..."
Exploration of Neural Machine Translation in Autoformalization of Mathematics in Mizar
Qingxiang Wang, Chad Brown, Cezary Kaliszyk, and Josef Urban
(University of Innsbruck, Austria; Czech Technical University in Prague, Czechia; University of Warsaw, Poland)
@InProceedings{CPP20p145,
author = {Qingxiang Wang and Chad Brown and Cezary Kaliszyk and Josef Urban},
title = {Exploration of Neural Machine Translation in Autoformalization of Mathematics in Mizar},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {145-144},
doi = {10.1145/3372885.3373827},
year = {2020},
}
Publisher's Version
Article: poplws20cppmain-p47-p doi:10.1145/3372885.3373827
|
| |
Van Doorn, Floris
|
CPP '20: "A Formal Proof of the Independence ..."
A Formal Proof of the Independence of the Continuum Hypothesis
Jesse Michael Han and Floris van Doorn
(University of Pittsburgh, USA)
@InProceedings{CPP20p487,
author = {Jesse Michael Han and Floris van Doorn},
title = {A Formal Proof of the Independence of the Continuum Hypothesis},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {487-486},
doi = {10.1145/3372885.3373826},
year = {2020},
}
Publisher's Version
Article: poplws20cppmain-p36-p doi:10.1145/3372885.3373826
|
| |
Veltri, Niccolò |
CPP '20: "Formalizing 𝜋-Calculus ..."
Formalizing 𝜋-Calculus in Guarded Cubical Agda
Niccolò Veltri and Andrea Vezzosi
(Tallinn University of Technology, Estonia; IT University of Copenhagen, Denmark)
@InProceedings{CPP20p379,
author = {Niccolò Veltri and Andrea Vezzosi},
title = {Formalizing 𝜋-Calculus in Guarded Cubical Agda},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {379-378},
doi = {10.1145/3372885.3373814},
year = {2020},
}
Publisher's Version
Article: poplws20cppmain-p46-p doi:10.1145/3372885.3373814
|
| |
Vezzosi, Andrea |
CPP '20: "Formalizing 𝜋-Calculus ..."
Formalizing 𝜋-Calculus in Guarded Cubical Agda
Niccolò Veltri and Andrea Vezzosi
(Tallinn University of Technology, Estonia; IT University of Copenhagen, Denmark)
@InProceedings{CPP20p379,
author = {Niccolò Veltri and Andrea Vezzosi},
title = {Formalizing 𝜋-Calculus in Guarded Cubical Agda},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {379-378},
doi = {10.1145/3372885.3373814},
year = {2020},
}
Publisher's Version
Article: poplws20cppmain-p46-p doi:10.1145/3372885.3373814
|
| |
Visser, Eelco |
CPP '20: "Intrinsically-Typed Definitional ..."
Intrinsically-Typed Definitional Interpreters for Linear, Session-Typed Languages
Arjen Rouvoet, Casper Bach Poulsen, Robbert Krebbers, and Eelco Visser
(Delft University of Technology, Netherlands)
@InProceedings{CPP20p397,
author = {Arjen Rouvoet and Casper Bach Poulsen and Robbert Krebbers and Eelco Visser},
title = {Intrinsically-Typed Definitional Interpreters for Linear, Session-Typed Languages},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {397-396},
doi = {10.1145/3372885.3373818},
year = {2020},
}
Publisher's Version
Published Artifact
Artifacts Available
Article: poplws20cppmain-p83-p doi:10.1145/3372885.3373818
|
| |
Wang, Qingxiang
|
CPP '20: "Exploration of Neural Machine ..."
Exploration of Neural Machine Translation in Autoformalization of Mathematics in Mizar
Qingxiang Wang, Chad Brown, Cezary Kaliszyk, and Josef Urban
(University of Innsbruck, Austria; Czech Technical University in Prague, Czechia; University of Warsaw, Poland)
@InProceedings{CPP20p145,
author = {Qingxiang Wang and Chad Brown and Cezary Kaliszyk and Josef Urban},
title = {Exploration of Neural Machine Translation in Autoformalization of Mathematics in Mizar},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {145-144},
doi = {10.1145/3372885.3373827},
year = {2020},
}
Publisher's Version
Article: poplws20cppmain-p47-p doi:10.1145/3372885.3373827
|
| |
Wuttke, Maximilian |
CPP '20: "Verified Programming of Turing ..."
Verified Programming of Turing Machines in Coq
Yannick Forster, Fabian Kunze, and Maximilian Wuttke
(Saarland University, Germany)
@InProceedings{CPP20p181,
author = {Yannick Forster and Fabian Kunze and Maximilian Wuttke},
title = {Verified Programming of Turing Machines in Coq},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {181-180},
doi = {10.1145/3372885.3373816},
year = {2020},
}
Publisher's Version
Article: poplws20cppmain-p63-p doi:10.1145/3372885.3373816
|
| |
Xu, Chuangjie
|
CPP '20: "Three Equivalent Ordinal Notation ..."
Three Equivalent Ordinal Notation Systems in Cubical Agda
Fredrik Nordvall Forsberg, Chuangjie Xu, and Neil Ghani
(University of Strathclyde, UK; LMU Munich, Germany)
@InProceedings{CPP20p253,
author = {Fredrik Nordvall Forsberg and Chuangjie Xu and Neil Ghani},
title = {Three Equivalent Ordinal Notation Systems in Cubical Agda},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {253-252},
doi = {10.1145/3372885.3373835},
year = {2020},
}
Publisher's Version
Published Artifact
Artifacts Available
Article: poplws20cppmain-p74-p doi:10.1145/3372885.3373835
|
| |
Zakowski, Yannick
|
CPP '20: "An Equational Theory for Weak ..."
An Equational Theory for Weak Bisimulation via Generalized Parameterized Coinduction
Yannick Zakowski, Paul He, Chung-Kil Hur, and Steve Zdancewic
(University of Pennsylvania, USA; Seoul National University, South Korea)
@InProceedings{CPP20p127,
author = {Yannick Zakowski and Paul He and Chung-Kil Hur and Steve Zdancewic},
title = {An Equational Theory for Weak Bisimulation via Generalized Parameterized Coinduction},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {127-126},
doi = {10.1145/3372885.3373813},
year = {2020},
}
Publisher's Version
Article: poplws20cppmain-p44-p doi:10.1145/3372885.3373813
|
| |
Zdancewic, Steve |
CPP '20: "An Equational Theory for Weak ..."
An Equational Theory for Weak Bisimulation via Generalized Parameterized Coinduction
Yannick Zakowski, Paul He, Chung-Kil Hur, and Steve Zdancewic
(University of Pennsylvania, USA; Seoul National University, South Korea)
@InProceedings{CPP20p127,
author = {Yannick Zakowski and Paul He and Chung-Kil Hur and Steve Zdancewic},
title = {An Equational Theory for Weak Bisimulation via Generalized Parameterized Coinduction},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {127-126},
doi = {10.1145/3372885.3373813},
year = {2020},
}
Publisher's Version
Article: poplws20cppmain-p44-p doi:10.1145/3372885.3373813
|