| |
Batz, Kevin
|
Proc. ACM Program. Lang., vol. 6, issue OOPSLA1: "Weighted Programming: A Programming ..."
Weighted Programming: A Programming Paradigm for Specifying Mathematical Models
Kevin Batz, Adrian Gallus, Benjamin Lucien Kaminski, Joost-Pieter Katoen, and Tobias Winkler
(RWTH Aachen University, Germany; Saarland University, Germany; University College London, UK)
 Publisher's Version
|
| |
Bell, Christian J. |
Proc. ACM Program. Lang., vol. 6, issue OOPSLA1: "C4: Verified Transactional ..."
C4: Verified Transactional Objects
Mohsen Lesani, Li-yao Xia, Anders Kaseorg, Christian J. Bell, Adam Chlipala, Benjamin C. Pierce, and Steve Zdancewic
(University of California at Riverside, USA; University of Pennsylvania, USA; Massachusetts Institute of Technology, USA)
Publisher's Version
 Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
Benzaken, Véronique |
Proc. ACM Program. Lang., vol. 6, issue OOPSLA1: "Translating Canonical SQL ..."
Translating Canonical SQL to Imperative Code in Coq
Véronique Benzaken, Évelyne Contejean, Mohammed Houssem Hachmaoui, Chantal Keller, Louis Mandel, Avraham Shinnar, and Jérôme Siméon
(LMF, France; Université Paris-Saclay, France; CNRS, France; IBM Research, USA; Docusign, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
|
| |
Berdine, Josh |
Proc. ACM Program. Lang., vol. 6, issue OOPSLA1: "Finding Real Bugs in Big Programs ..."
Finding Real Bugs in Big Programs with Incorrectness Logic
Quang Loc Le, Azalea Raad, Jules Villard, Josh Berdine, Derek Dreyer, and Peter W. O'Hearn
(University College London, UK; Meta, UK; Imperial College London, UK; MPI-SWS, Germany)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
Birkedal, Lars |
Proc. ACM Program. Lang., vol. 6, issue OOPSLA1: "Le Temps des Cerises: Efficient ..."
Le Temps des Cerises: Efficient Temporal Stack Safety on Capability Machines using Directed Capabilities
Aïna Linn Georges, Alix Trieu, and Lars Birkedal
(Aarhus University, Denmark; ANSSI, France)
Publisher's Version
Published Artifact
Archive submitted (440 kB)
Artifacts Available
Artifacts Reusable
|
| |
Bornholt, James |
Proc. ACM Program. Lang., vol. 6, issue OOPSLA1: "Synthesizing Fine-Grained ..."
Synthesizing Fine-Grained Synchronization Protocols for Implicit Monitors
Kostas Ferles, Benjamin Sepanski, Rahul Krishnan, James Bornholt, and Işil Dillig
(University of Texas at Austin, USA)
Publisher's Version
|
| |
Boruch-Gruszecki, Aleksander |
Proc. ACM Program. Lang., vol. 6, issue OOPSLA1: "Effects, Capabilities, and ..."
Effects, Capabilities, and Boxes: From Scope-Based Reasoning to Type-Based Reasoning and Back
Jonathan Immanuel Brachthäuser, Philipp Schuster, Edward Lee, and Aleksander Boruch-Gruszecki
(University of Tübingen, Germany; University of Waterloo, Canada; EPFL, Switzerland)
Publisher's Version
Published Artifact
Archive submitted (1.1 MB)
Artifacts Available
Artifacts Reusable
|
| |
Brachthäuser, Jonathan Immanuel |
Proc. ACM Program. Lang., vol. 6, issue OOPSLA1: "Effects, Capabilities, and ..."
Effects, Capabilities, and Boxes: From Scope-Based Reasoning to Type-Based Reasoning and Back
Jonathan Immanuel Brachthäuser, Philipp Schuster, Edward Lee, and Aleksander Boruch-Gruszecki
(University of Tübingen, Germany; University of Waterloo, Canada; EPFL, Switzerland)
Publisher's Version
Published Artifact
Archive submitted (1.1 MB)
Artifacts Available
Artifacts Reusable
|
| |
Cameron, Jonathan
|
Proc. ACM Program. Lang., vol. 6, issue OOPSLA1: "Linear Types for Large-Scale ..."
Linear Types for Large-Scale Systems Verification
Jialin Li, Andrea Lattuada, Yi Zhou, Jonathan Cameron, Jon Howell, Bryan Parno, and Chris Hawblitzel
(University of Washington, USA; ETH Zurich, Switzerland; Carnegie Mellon University, USA; VMware Research, USA; Microsoft Research, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
Chen, Yanju |
Proc. ACM Program. Lang., vol. 6, issue OOPSLA1: "Automated Transpilation of ..."
Automated Transpilation of Imperative to Functional Code using Neural-Guided Program Synthesis
Benjamin Mariano, Yanju Chen, Yu Feng, Greg Durrett, and Işil Dillig
(University of Texas at Austin, USA; University of California at Santa Barbara, USA)
Publisher's Version
|
| |
Chlipala, Adam |
Proc. ACM Program. Lang., vol. 6, issue OOPSLA1: "C4: Verified Transactional ..."
C4: Verified Transactional Objects
Mohsen Lesani, Li-yao Xia, Anders Kaseorg, Christian J. Bell, Adam Chlipala, Benjamin C. Pierce, and Steve Zdancewic
(University of California at Riverside, USA; University of Pennsylvania, USA; Massachusetts Institute of Technology, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
Clément, Basile |
Proc. ACM Program. Lang., vol. 6, issue OOPSLA1: "End-to-End Translation Validation ..."
End-to-End Translation Validation for the Halide Language
Basile Clément and Albert Cohen
(Inria, France; ENS Paris, France; Google, France)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
|
| |
Cohen, Albert |
Proc. ACM Program. Lang., vol. 6, issue OOPSLA1: "End-to-End Translation Validation ..."
End-to-End Translation Validation for the Halide Language
Basile Clément and Albert Cohen
(Inria, France; ENS Paris, France; Google, France)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
|
| |
Contejean, Évelyne |
Proc. ACM Program. Lang., vol. 6, issue OOPSLA1: "Translating Canonical SQL ..."
Translating Canonical SQL to Imperative Code in Coq
Véronique Benzaken, Évelyne Contejean, Mohammed Houssem Hachmaoui, Chantal Keller, Louis Mandel, Avraham Shinnar, and Jérôme Siméon
(LMF, France; Université Paris-Saclay, France; CNRS, France; IBM Research, USA; Docusign, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
|
| |
Deng, Yinlin
|
Proc. ACM Program. Lang., vol. 6, issue OOPSLA1: "Coverage-Guided Tensor Compiler ..."
Coverage-Guided Tensor Compiler Fuzzing with Joint IR-Pass Mutation
Jiawei Liu, Yuxiang Wei, Sen Yang, Yinlin Deng, and Lingming Zhang
(University of Illinois at Urbana-Champaign, USA; Tongji University, China; Fudan University, China)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
Devriese, Dominique |
Proc. ACM Program. Lang., vol. 6, issue OOPSLA1: "Plausible Sealing for Gradual ..."
Plausible Sealing for Gradual Parametricity
Elizabeth Labrada, Matías Toro, Éric Tanter, and Dominique Devriese
(University of Chile, Chile; KU Leuven, Belgium)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
Proc. ACM Program. Lang., vol. 6, issue OOPSLA1: "Purity of an ST Monad: Full ..."
Purity of an ST Monad: Full Abstraction by Semantically Typed Back-Translation
Koen Jacobs, Dominique Devriese, and Amin Timany
(KU Leuven, Belgium; Aarhus University, Denmark)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
Dillig, Işil |
Proc. ACM Program. Lang., vol. 6, issue OOPSLA1: "Synthesizing Fine-Grained ..."
Synthesizing Fine-Grained Synchronization Protocols for Implicit Monitors
Kostas Ferles, Benjamin Sepanski, Rahul Krishnan, James Bornholt, and Işil Dillig
(University of Texas at Austin, USA)
Publisher's Version
Proc. ACM Program. Lang., vol. 6, issue OOPSLA1: "Automated Transpilation of ..."
Automated Transpilation of Imperative to Functional Code using Neural-Guided Program Synthesis
Benjamin Mariano, Yanju Chen, Yu Feng, Greg Durrett, and Işil Dillig
(University of Texas at Austin, USA; University of California at Santa Barbara, USA)
Publisher's Version
|
| |
Dreyer, Derek |
Proc. ACM Program. Lang., vol. 6, issue OOPSLA1: "Finding Real Bugs in Big Programs ..."
Finding Real Bugs in Big Programs with Incorrectness Logic
Quang Loc Le, Azalea Raad, Jules Villard, Josh Berdine, Derek Dreyer, and Peter W. O'Hearn
(University College London, UK; Meta, UK; Imperial College London, UK; MPI-SWS, Germany)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
Durrett, Greg |
Proc. ACM Program. Lang., vol. 6, issue OOPSLA1: "Automated Transpilation of ..."
Automated Transpilation of Imperative to Functional Code using Neural-Guided Program Synthesis
Benjamin Mariano, Yanju Chen, Yu Feng, Greg Durrett, and Işil Dillig
(University of Texas at Austin, USA; University of California at Santa Barbara, USA)
Publisher's Version
|
| |
Dyer, Tristan |
Proc. ACM Program. Lang., vol. 6, issue OOPSLA1: "Applying Cognitive Principles ..."
Applying Cognitive Principles to Model-Finding Output: The Positive Value of Negative Information
Tristan Dyer, Tim Nelson, Kathi Fisler, and Shriram Krishnamurthi
(Brown University, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
Eline, Aaron
|
Proc. ACM Program. Lang., vol. 6, issue OOPSLA1: "C to Checked C by 3C ..."
C to Checked C by 3C
Aravind Machiry, John Kastner, Matt McCutchen, Aaron Eline, Kyle Headley, and Michael Hicks
(Purdue University, USA; Amazon, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
Feng, Yu
|
Proc. ACM Program. Lang., vol. 6, issue OOPSLA1: "Automated Transpilation of ..."
Automated Transpilation of Imperative to Functional Code using Neural-Guided Program Synthesis
Benjamin Mariano, Yanju Chen, Yu Feng, Greg Durrett, and Işil Dillig
(University of Texas at Austin, USA; University of California at Santa Barbara, USA)
Publisher's Version
|
| |
Ferles, Kostas |
Proc. ACM Program. Lang., vol. 6, issue OOPSLA1: "Synthesizing Fine-Grained ..."
Synthesizing Fine-Grained Synchronization Protocols for Implicit Monitors
Kostas Ferles, Benjamin Sepanski, Rahul Krishnan, James Bornholt, and Işil Dillig
(University of Texas at Austin, USA)
Publisher's Version
|
| |
Fisler, Kathi |
Proc. ACM Program. Lang., vol. 6, issue OOPSLA1: "Applying Cognitive Principles ..."
Applying Cognitive Principles to Model-Finding Output: The Positive Value of Negative Information
Tristan Dyer, Tim Nelson, Kathi Fisler, and Shriram Krishnamurthi
(Brown University, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
Gallus, Adrian
|
Proc. ACM Program. Lang., vol. 6, issue OOPSLA1: "Weighted Programming: A Programming ..."
Weighted Programming: A Programming Paradigm for Specifying Mathematical Models
Kevin Batz, Adrian Gallus, Benjamin Lucien Kaminski, Joost-Pieter Katoen, and Tobias Winkler
(RWTH Aachen University, Germany; Saarland University, Germany; University College London, UK)
Publisher's Version
|
| |
Georges, Aïna Linn |
Proc. ACM Program. Lang., vol. 6, issue OOPSLA1: "Le Temps des Cerises: Efficient ..."
Le Temps des Cerises: Efficient Temporal Stack Safety on Capability Machines using Directed Capabilities
Aïna Linn Georges, Alix Trieu, and Lars Birkedal
(Aarhus University, Denmark; ANSSI, France)
Publisher's Version
Published Artifact
Archive submitted (440 kB)
Artifacts Available
Artifacts Reusable
|
| |
Grech, Neville |
Proc. ACM Program. Lang., vol. 6, issue OOPSLA1: "Elipmoc: Advanced Decompilation ..."
Elipmoc: Advanced Decompilation of Ethereum Smart Contracts
Neville Grech, Sifis Lagouvardos, Ilias Tsatiris, and Yannis Smaragdakis
(University of Malta, Malta; University of Athens, Greece)
Publisher's Version
Artifacts Reusable
|
| |
Hachmaoui, Mohammed Houssem
|
Proc. ACM Program. Lang., vol. 6, issue OOPSLA1: "Translating Canonical SQL ..."
Translating Canonical SQL to Imperative Code in Coq
Véronique Benzaken, Évelyne Contejean, Mohammed Houssem Hachmaoui, Chantal Keller, Louis Mandel, Avraham Shinnar, and Jérôme Siméon
(LMF, France; Université Paris-Saclay, France; CNRS, France; IBM Research, USA; Docusign, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
|
| |
Hawblitzel, Chris |
Proc. ACM Program. Lang., vol. 6, issue OOPSLA1: "Linear Types for Large-Scale ..."
Linear Types for Large-Scale Systems Verification
Jialin Li, Andrea Lattuada, Yi Zhou, Jonathan Cameron, Jon Howell, Bryan Parno, and Chris Hawblitzel
(University of Washington, USA; ETH Zurich, Switzerland; Carnegie Mellon University, USA; VMware Research, USA; Microsoft Research, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
Headley, Kyle |
Proc. ACM Program. Lang., vol. 6, issue OOPSLA1: "C to Checked C by 3C ..."
C to Checked C by 3C
Aravind Machiry, John Kastner, Matt McCutchen, Aaron Eline, Kyle Headley, and Michael Hicks
(Purdue University, USA; Amazon, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
Hicks, Michael |
Proc. ACM Program. Lang., vol. 6, issue OOPSLA1: "C to Checked C by 3C ..."
C to Checked C by 3C
Aravind Machiry, John Kastner, Matt McCutchen, Aaron Eline, Kyle Headley, and Michael Hicks
(Purdue University, USA; Amazon, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
Howell, Jon |
Proc. ACM Program. Lang., vol. 6, issue OOPSLA1: "Linear Types for Large-Scale ..."
Linear Types for Large-Scale Systems Verification
Jialin Li, Andrea Lattuada, Yi Zhou, Jonathan Cameron, Jon Howell, Bryan Parno, and Chris Hawblitzel
(University of Washington, USA; ETH Zurich, Switzerland; Carnegie Mellon University, USA; VMware Research, USA; Microsoft Research, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
Huang, Jeff |
Proc. ACM Program. Lang., vol. 6, issue OOPSLA1: "SHARP: Fast Incremental Context-Sensitive ..."
SHARP: Fast Incremental Context-Sensitive Pointer Analysis for Java
Bozhen Liu and Jeff Huang
(Texas A&M University, USA)
Publisher's Version
|
| |
Huot, Mathieu |
Proc. ACM Program. Lang., vol. 6, issue OOPSLA1: "Functional Collection Programming ..."
Functional Collection Programming with Semi-ring Dictionaries
Amir Shaikhha, Mathieu Huot, Jaclyn Smith, and Dan Olteanu
(University of Edinburgh, UK; University of Oxford, UK; University of Zurich, Switzerland)
Publisher's Version
|
| |
Jacobs, Koen
|
Proc. ACM Program. Lang., vol. 6, issue OOPSLA1: "Purity of an ST Monad: Full ..."
Purity of an ST Monad: Full Abstraction by Semantically Typed Back-Translation
Koen Jacobs, Dominique Devriese, and Amin Timany
(KU Leuven, Belgium; Aarhus University, Denmark)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
Jiang, Hanru |
Proc. ACM Program. Lang., vol. 6, issue OOPSLA1: "On Incorrectness Logic for ..."
On Incorrectness Logic for Quantum Programs
Peng Yan, Hanru Jiang, and Nengkun Yu
(University of Technology Sydney, Australia; BIMSA, China)
Publisher's Version
|
| |
Kaminski, Benjamin Lucien
|
Proc. ACM Program. Lang., vol. 6, issue OOPSLA1: "Weighted Programming: A Programming ..."
Weighted Programming: A Programming Paradigm for Specifying Mathematical Models
Kevin Batz, Adrian Gallus, Benjamin Lucien Kaminski, Joost-Pieter Katoen, and Tobias Winkler
(RWTH Aachen University, Germany; Saarland University, Germany; University College London, UK)
Publisher's Version
Proc. ACM Program. Lang., vol. 6, issue OOPSLA1: "Quantitative Strongest Post: ..."
Quantitative Strongest Post: A Calculus for Reasoning about the Flow of Quantitative Information
Linpeng Zhang and Benjamin Lucien Kaminski
(University College London, UK; Saarland University, Germany)
Publisher's Version
|
| |
Kaseorg, Anders |
Proc. ACM Program. Lang., vol. 6, issue OOPSLA1: "C4: Verified Transactional ..."
C4: Verified Transactional Objects
Mohsen Lesani, Li-yao Xia, Anders Kaseorg, Christian J. Bell, Adam Chlipala, Benjamin C. Pierce, and Steve Zdancewic
(University of California at Riverside, USA; University of Pennsylvania, USA; Massachusetts Institute of Technology, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
Kastner, John |
Proc. ACM Program. Lang., vol. 6, issue OOPSLA1: "C to Checked C by 3C ..."
C to Checked C by 3C
Aravind Machiry, John Kastner, Matt McCutchen, Aaron Eline, Kyle Headley, and Michael Hicks
(Purdue University, USA; Amazon, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
Katoen, Joost-Pieter |
Proc. ACM Program. Lang., vol. 6, issue OOPSLA1: "Weighted Programming: A Programming ..."
Weighted Programming: A Programming Paradigm for Specifying Mathematical Models
Kevin Batz, Adrian Gallus, Benjamin Lucien Kaminski, Joost-Pieter Katoen, and Tobias Winkler
(RWTH Aachen University, Germany; Saarland University, Germany; University College London, UK)
Publisher's Version
|
| |
Keller, Chantal |
Proc. ACM Program. Lang., vol. 6, issue OOPSLA1: "Translating Canonical SQL ..."
Translating Canonical SQL to Imperative Code in Coq
Véronique Benzaken, Évelyne Contejean, Mohammed Houssem Hachmaoui, Chantal Keller, Louis Mandel, Avraham Shinnar, and Jérôme Siméon
(LMF, France; Université Paris-Saclay, France; CNRS, France; IBM Research, USA; Docusign, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
|
| |
Krishnamurthi, Shriram |
Proc. ACM Program. Lang., vol. 6, issue OOPSLA1: "Applying Cognitive Principles ..."
Applying Cognitive Principles to Model-Finding Output: The Positive Value of Negative Information
Tristan Dyer, Tim Nelson, Kathi Fisler, and Shriram Krishnamurthi
(Brown University, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
Krishnan, Rahul |
Proc. ACM Program. Lang., vol. 6, issue OOPSLA1: "Synthesizing Fine-Grained ..."
Synthesizing Fine-Grained Synchronization Protocols for Implicit Monitors
Kostas Ferles, Benjamin Sepanski, Rahul Krishnan, James Bornholt, and Işil Dillig
(University of Texas at Austin, USA)
Publisher's Version
|
| |
Labrada, Elizabeth
|
Proc. ACM Program. Lang., vol. 6, issue OOPSLA1: "Plausible Sealing for Gradual ..."
Plausible Sealing for Gradual Parametricity
Elizabeth Labrada, Matías Toro, Éric Tanter, and Dominique Devriese
(University of Chile, Chile; KU Leuven, Belgium)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
Lagouvardos, Sifis |
Proc. ACM Program. Lang., vol. 6, issue OOPSLA1: "Elipmoc: Advanced Decompilation ..."
Elipmoc: Advanced Decompilation of Ethereum Smart Contracts
Neville Grech, Sifis Lagouvardos, Ilias Tsatiris, and Yannis Smaragdakis
(University of Malta, Malta; University of Athens, Greece)
Publisher's Version
Artifacts Reusable
|
| |
Lattuada, Andrea |
Proc. ACM Program. Lang., vol. 6, issue OOPSLA1: "Linear Types for Large-Scale ..."
Linear Types for Large-Scale Systems Verification
Jialin Li, Andrea Lattuada, Yi Zhou, Jonathan Cameron, Jon Howell, Bryan Parno, and Chris Hawblitzel
(University of Washington, USA; ETH Zurich, Switzerland; Carnegie Mellon University, USA; VMware Research, USA; Microsoft Research, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
Le, Quang Loc |
Proc. ACM Program. Lang., vol. 6, issue OOPSLA1: "Finding Real Bugs in Big Programs ..."
Finding Real Bugs in Big Programs with Incorrectness Logic
Quang Loc Le, Azalea Raad, Jules Villard, Josh Berdine, Derek Dreyer, and Peter W. O'Hearn
(University College London, UK; Meta, UK; Imperial College London, UK; MPI-SWS, Germany)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
Lee, Edward |
Proc. ACM Program. Lang., vol. 6, issue OOPSLA1: "Effects, Capabilities, and ..."
Effects, Capabilities, and Boxes: From Scope-Based Reasoning to Type-Based Reasoning and Back
Jonathan Immanuel Brachthäuser, Philipp Schuster, Edward Lee, and Aleksander Boruch-Gruszecki
(University of Tübingen, Germany; University of Waterloo, Canada; EPFL, Switzerland)
Publisher's Version
Published Artifact
Archive submitted (1.1 MB)
Artifacts Available
Artifacts Reusable
|
| |
Lesani, Mohsen |
Proc. ACM Program. Lang., vol. 6, issue OOPSLA1: "C4: Verified Transactional ..."
C4: Verified Transactional Objects
Mohsen Lesani, Li-yao Xia, Anders Kaseorg, Christian J. Bell, Adam Chlipala, Benjamin C. Pierce, and Steve Zdancewic
(University of California at Riverside, USA; University of Pennsylvania, USA; Massachusetts Institute of Technology, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
Li, Jialin |
Proc. ACM Program. Lang., vol. 6, issue OOPSLA1: "Linear Types for Large-Scale ..."
Linear Types for Large-Scale Systems Verification
Jialin Li, Andrea Lattuada, Yi Zhou, Jonathan Cameron, Jon Howell, Bryan Parno, and Chris Hawblitzel
(University of Washington, USA; ETH Zurich, Switzerland; Carnegie Mellon University, USA; VMware Research, USA; Microsoft Research, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
Liu, Bozhen |
Proc. ACM Program. Lang., vol. 6, issue OOPSLA1: "SHARP: Fast Incremental Context-Sensitive ..."
SHARP: Fast Incremental Context-Sensitive Pointer Analysis for Java
Bozhen Liu and Jeff Huang
(Texas A&M University, USA)
Publisher's Version
|
| |
Liu, Jiawei |
Proc. ACM Program. Lang., vol. 6, issue OOPSLA1: "Coverage-Guided Tensor Compiler ..."
Coverage-Guided Tensor Compiler Fuzzing with Joint IR-Pass Mutation
Jiawei Liu, Yuxiang Wei, Sen Yang, Yinlin Deng, and Lingming Zhang
(University of Illinois at Urbana-Champaign, USA; Tongji University, China; Fudan University, China)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
Machiry, Aravind
|
Proc. ACM Program. Lang., vol. 6, issue OOPSLA1: "C to Checked C by 3C ..."
C to Checked C by 3C
Aravind Machiry, John Kastner, Matt McCutchen, Aaron Eline, Kyle Headley, and Michael Hicks
(Purdue University, USA; Amazon, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
Mandel, Louis |
Proc. ACM Program. Lang., vol. 6, issue OOPSLA1: "Translating Canonical SQL ..."
Translating Canonical SQL to Imperative Code in Coq
Véronique Benzaken, Évelyne Contejean, Mohammed Houssem Hachmaoui, Chantal Keller, Louis Mandel, Avraham Shinnar, and Jérôme Siméon
(LMF, France; Université Paris-Saclay, France; CNRS, France; IBM Research, USA; Docusign, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
|
| |
Mariano, Benjamin |
Proc. ACM Program. Lang., vol. 6, issue OOPSLA1: "Automated Transpilation of ..."
Automated Transpilation of Imperative to Functional Code using Neural-Guided Program Synthesis
Benjamin Mariano, Yanju Chen, Yu Feng, Greg Durrett, and Işil Dillig
(University of Texas at Austin, USA; University of California at Santa Barbara, USA)
Publisher's Version
|
| |
McCutchen, Matt |
Proc. ACM Program. Lang., vol. 6, issue OOPSLA1: "C to Checked C by 3C ..."
C to Checked C by 3C
Aravind Machiry, John Kastner, Matt McCutchen, Aaron Eline, Kyle Headley, and Michael Hicks
(Purdue University, USA; Amazon, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
Misailovic, Sasa |
Proc. ACM Program. Lang., vol. 6, issue OOPSLA1: "Proof Transfer for Fast Certification ..."
Proof Transfer for Fast Certification of Multiple Approximate Neural Networks
Shubham Ugare, Gagandeep Singh, and Sasa Misailovic
(University of Illinois at Urbana-Champaign, USA; VMware Research, USA)
Publisher's Version
|
| |
Nelson, Tim
|
Proc. ACM Program. Lang., vol. 6, issue OOPSLA1: "Applying Cognitive Principles ..."
Applying Cognitive Principles to Model-Finding Output: The Positive Value of Negative Information
Tristan Dyer, Tim Nelson, Kathi Fisler, and Shriram Krishnamurthi
(Brown University, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
O'Hearn, Peter W.
|
Proc. ACM Program. Lang., vol. 6, issue OOPSLA1: "Finding Real Bugs in Big Programs ..."
Finding Real Bugs in Big Programs with Incorrectness Logic
Quang Loc Le, Azalea Raad, Jules Villard, Josh Berdine, Derek Dreyer, and Peter W. O'Hearn
(University College London, UK; Meta, UK; Imperial College London, UK; MPI-SWS, Germany)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
Olteanu, Dan |
Proc. ACM Program. Lang., vol. 6, issue OOPSLA1: "Functional Collection Programming ..."
Functional Collection Programming with Semi-ring Dictionaries
Amir Shaikhha, Mathieu Huot, Jaclyn Smith, and Dan Olteanu
(University of Edinburgh, UK; University of Oxford, UK; University of Zurich, Switzerland)
Publisher's Version
|
| |
Paltenghi, Matteo
|
Proc. ACM Program. Lang., vol. 6, issue OOPSLA1: "Bugs in Quantum Computing ..."
Bugs in Quantum Computing Platforms: An Empirical Study
Matteo Paltenghi and Michael Pradel
(University of Stuttgart, Germany)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
Parno, Bryan |
Proc. ACM Program. Lang., vol. 6, issue OOPSLA1: "Linear Types for Large-Scale ..."
Linear Types for Large-Scale Systems Verification
Jialin Li, Andrea Lattuada, Yi Zhou, Jonathan Cameron, Jon Howell, Bryan Parno, and Chris Hawblitzel
(University of Washington, USA; ETH Zurich, Switzerland; Carnegie Mellon University, USA; VMware Research, USA; Microsoft Research, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
Pelsmaeker, Daniel A. A. |
Proc. ACM Program. Lang., vol. 6, issue OOPSLA1: "Language-Parametric Static ..."
Language-Parametric Static Semantic Code Completion
Daniel A. A. Pelsmaeker, Hendrik van Antwerpen, Casper Bach Poulsen, and Eelco Visser
(Delft University of Technology, Netherlands)
Publisher's Version
Published Artifact
Archive submitted (120 kB)
Artifacts Available
Artifacts Functional
|
| |
Pierce, Benjamin C. |
Proc. ACM Program. Lang., vol. 6, issue OOPSLA1: "C4: Verified Transactional ..."
C4: Verified Transactional Objects
Mohsen Lesani, Li-yao Xia, Anders Kaseorg, Christian J. Bell, Adam Chlipala, Benjamin C. Pierce, and Steve Zdancewic
(University of California at Riverside, USA; University of Pennsylvania, USA; Massachusetts Institute of Technology, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
Poulsen, Casper Bach |
Proc. ACM Program. Lang., vol. 6, issue OOPSLA1: "Language-Parametric Static ..."
Language-Parametric Static Semantic Code Completion
Daniel A. A. Pelsmaeker, Hendrik van Antwerpen, Casper Bach Poulsen, and Eelco Visser
(Delft University of Technology, Netherlands)
Publisher's Version
Published Artifact
Archive submitted (120 kB)
Artifacts Available
Artifacts Functional
|
| |
Pradel, Michael |
Proc. ACM Program. Lang., vol. 6, issue OOPSLA1: "Bugs in Quantum Computing ..."
Bugs in Quantum Computing Platforms: An Empirical Study
Matteo Paltenghi and Michael Pradel
(University of Stuttgart, Germany)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
Raad, Azalea
|
Proc. ACM Program. Lang., vol. 6, issue OOPSLA1: "Finding Real Bugs in Big Programs ..."
Finding Real Bugs in Big Programs with Incorrectness Logic
Quang Loc Le, Azalea Raad, Jules Villard, Josh Berdine, Derek Dreyer, and Peter W. O'Hearn
(University College London, UK; Meta, UK; Imperial College London, UK; MPI-SWS, Germany)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
Schuster, Philipp
|
Proc. ACM Program. Lang., vol. 6, issue OOPSLA1: "Effects, Capabilities, and ..."
Effects, Capabilities, and Boxes: From Scope-Based Reasoning to Type-Based Reasoning and Back
Jonathan Immanuel Brachthäuser, Philipp Schuster, Edward Lee, and Aleksander Boruch-Gruszecki
(University of Tübingen, Germany; University of Waterloo, Canada; EPFL, Switzerland)
Publisher's Version
Published Artifact
Archive submitted (1.1 MB)
Artifacts Available
Artifacts Reusable
|
| |
Sepanski, Benjamin |
Proc. ACM Program. Lang., vol. 6, issue OOPSLA1: "Synthesizing Fine-Grained ..."
Synthesizing Fine-Grained Synchronization Protocols for Implicit Monitors
Kostas Ferles, Benjamin Sepanski, Rahul Krishnan, James Bornholt, and Işil Dillig
(University of Texas at Austin, USA)
Publisher's Version
|
| |
Shaikhha, Amir |
Proc. ACM Program. Lang., vol. 6, issue OOPSLA1: "Functional Collection Programming ..."
Functional Collection Programming with Semi-ring Dictionaries
Amir Shaikhha, Mathieu Huot, Jaclyn Smith, and Dan Olteanu
(University of Edinburgh, UK; University of Oxford, UK; University of Zurich, Switzerland)
Publisher's Version
|
| |
Shi, Qingkai |
Proc. ACM Program. Lang., vol. 6, issue OOPSLA1: "Complexity-Guided Container ..."
Complexity-Guided Container Replacement Synthesis
Chengpeng Wang, Peisen Yao, Wensheng Tang, Qingkai Shi, and Charles Zhang
(Hong Kong University of Science and Technology, China; Ant Group, China)
Publisher's Version
|
| |
Shinnar, Avraham |
Proc. ACM Program. Lang., vol. 6, issue OOPSLA1: "Translating Canonical SQL ..."
Translating Canonical SQL to Imperative Code in Coq
Véronique Benzaken, Évelyne Contejean, Mohammed Houssem Hachmaoui, Chantal Keller, Louis Mandel, Avraham Shinnar, and Jérôme Siméon
(LMF, France; Université Paris-Saclay, France; CNRS, France; IBM Research, USA; Docusign, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
|
| |
Siméon, Jérôme |
Proc. ACM Program. Lang., vol. 6, issue OOPSLA1: "Translating Canonical SQL ..."
Translating Canonical SQL to Imperative Code in Coq
Véronique Benzaken, Évelyne Contejean, Mohammed Houssem Hachmaoui, Chantal Keller, Louis Mandel, Avraham Shinnar, and Jérôme Siméon
(LMF, France; Université Paris-Saclay, France; CNRS, France; IBM Research, USA; Docusign, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
|
| |
Singh, Gagandeep |
Proc. ACM Program. Lang., vol. 6, issue OOPSLA1: "Proof Transfer for Fast Certification ..."
Proof Transfer for Fast Certification of Multiple Approximate Neural Networks
Shubham Ugare, Gagandeep Singh, and Sasa Misailovic
(University of Illinois at Urbana-Champaign, USA; VMware Research, USA)
Publisher's Version
|
| |
Smaragdakis, Yannis |
Proc. ACM Program. Lang., vol. 6, issue OOPSLA1: "Elipmoc: Advanced Decompilation ..."
Elipmoc: Advanced Decompilation of Ethereum Smart Contracts
Neville Grech, Sifis Lagouvardos, Ilias Tsatiris, and Yannis Smaragdakis
(University of Malta, Malta; University of Athens, Greece)
Publisher's Version
Artifacts Reusable
|
| |
Smith, Jaclyn |
Proc. ACM Program. Lang., vol. 6, issue OOPSLA1: "Functional Collection Programming ..."
Functional Collection Programming with Semi-ring Dictionaries
Amir Shaikhha, Mathieu Huot, Jaclyn Smith, and Dan Olteanu
(University of Edinburgh, UK; University of Oxford, UK; University of Zurich, Switzerland)
Publisher's Version
|
| |
Tang, Wensheng
|
Proc. ACM Program. Lang., vol. 6, issue OOPSLA1: "Complexity-Guided Container ..."
Complexity-Guided Container Replacement Synthesis
Chengpeng Wang, Peisen Yao, Wensheng Tang, Qingkai Shi, and Charles Zhang
(Hong Kong University of Science and Technology, China; Ant Group, China)
Publisher's Version
|
| |
Tanter, Éric |
Proc. ACM Program. Lang., vol. 6, issue OOPSLA1: "Plausible Sealing for Gradual ..."
Plausible Sealing for Gradual Parametricity
Elizabeth Labrada, Matías Toro, Éric Tanter, and Dominique Devriese
(University of Chile, Chile; KU Leuven, Belgium)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
Timany, Amin |
Proc. ACM Program. Lang., vol. 6, issue OOPSLA1: "Purity of an ST Monad: Full ..."
Purity of an ST Monad: Full Abstraction by Semantically Typed Back-Translation
Koen Jacobs, Dominique Devriese, and Amin Timany
(KU Leuven, Belgium; Aarhus University, Denmark)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
Toro, Matías |
Proc. ACM Program. Lang., vol. 6, issue OOPSLA1: "Plausible Sealing for Gradual ..."
Plausible Sealing for Gradual Parametricity
Elizabeth Labrada, Matías Toro, Éric Tanter, and Dominique Devriese
(University of Chile, Chile; KU Leuven, Belgium)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
Trieu, Alix |
Proc. ACM Program. Lang., vol. 6, issue OOPSLA1: "Le Temps des Cerises: Efficient ..."
Le Temps des Cerises: Efficient Temporal Stack Safety on Capability Machines using Directed Capabilities
Aïna Linn Georges, Alix Trieu, and Lars Birkedal
(Aarhus University, Denmark; ANSSI, France)
Publisher's Version
Published Artifact
Archive submitted (440 kB)
Artifacts Available
Artifacts Reusable
|
| |
Tsatiris, Ilias |
Proc. ACM Program. Lang., vol. 6, issue OOPSLA1: "Elipmoc: Advanced Decompilation ..."
Elipmoc: Advanced Decompilation of Ethereum Smart Contracts
Neville Grech, Sifis Lagouvardos, Ilias Tsatiris, and Yannis Smaragdakis
(University of Malta, Malta; University of Athens, Greece)
Publisher's Version
Artifacts Reusable
|
| |
Ugare, Shubham
|
Proc. ACM Program. Lang., vol. 6, issue OOPSLA1: "Proof Transfer for Fast Certification ..."
Proof Transfer for Fast Certification of Multiple Approximate Neural Networks
Shubham Ugare, Gagandeep Singh, and Sasa Misailovic
(University of Illinois at Urbana-Champaign, USA; VMware Research, USA)
Publisher's Version
|
| |
Van Antwerpen, Hendrik
|
Proc. ACM Program. Lang., vol. 6, issue OOPSLA1: "Language-Parametric Static ..."
Language-Parametric Static Semantic Code Completion
Daniel A. A. Pelsmaeker, Hendrik van Antwerpen, Casper Bach Poulsen, and Eelco Visser
(Delft University of Technology, Netherlands)
Publisher's Version
Published Artifact
Archive submitted (120 kB)
Artifacts Available
Artifacts Functional
|
| |
Villard, Jules |
Proc. ACM Program. Lang., vol. 6, issue OOPSLA1: "Finding Real Bugs in Big Programs ..."
Finding Real Bugs in Big Programs with Incorrectness Logic
Quang Loc Le, Azalea Raad, Jules Villard, Josh Berdine, Derek Dreyer, and Peter W. O'Hearn
(University College London, UK; Meta, UK; Imperial College London, UK; MPI-SWS, Germany)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
Visser, Eelco |
Proc. ACM Program. Lang., vol. 6, issue OOPSLA1: "Language-Parametric Static ..."
Language-Parametric Static Semantic Code Completion
Daniel A. A. Pelsmaeker, Hendrik van Antwerpen, Casper Bach Poulsen, and Eelco Visser
(Delft University of Technology, Netherlands)
Publisher's Version
Published Artifact
Archive submitted (120 kB)
Artifacts Available
Artifacts Functional
|
| |
Wang, Chengpeng
|
Proc. ACM Program. Lang., vol. 6, issue OOPSLA1: "Complexity-Guided Container ..."
Complexity-Guided Container Replacement Synthesis
Chengpeng Wang, Peisen Yao, Wensheng Tang, Qingkai Shi, and Charles Zhang
(Hong Kong University of Science and Technology, China; Ant Group, China)
Publisher's Version
|
| |
Wei, Yuxiang |
Proc. ACM Program. Lang., vol. 6, issue OOPSLA1: "Coverage-Guided Tensor Compiler ..."
Coverage-Guided Tensor Compiler Fuzzing with Joint IR-Pass Mutation
Jiawei Liu, Yuxiang Wei, Sen Yang, Yinlin Deng, and Lingming Zhang
(University of Illinois at Urbana-Champaign, USA; Tongji University, China; Fudan University, China)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
Winkler, Tobias |
Proc. ACM Program. Lang., vol. 6, issue OOPSLA1: "Weighted Programming: A Programming ..."
Weighted Programming: A Programming Paradigm for Specifying Mathematical Models
Kevin Batz, Adrian Gallus, Benjamin Lucien Kaminski, Joost-Pieter Katoen, and Tobias Winkler
(RWTH Aachen University, Germany; Saarland University, Germany; University College London, UK)
Publisher's Version
|
| |
Xia, Li-yao
|
Proc. ACM Program. Lang., vol. 6, issue OOPSLA1: "C4: Verified Transactional ..."
C4: Verified Transactional Objects
Mohsen Lesani, Li-yao Xia, Anders Kaseorg, Christian J. Bell, Adam Chlipala, Benjamin C. Pierce, and Steve Zdancewic
(University of California at Riverside, USA; University of Pennsylvania, USA; Massachusetts Institute of Technology, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
Yan, Peng
|
Proc. ACM Program. Lang., vol. 6, issue OOPSLA1: "On Incorrectness Logic for ..."
On Incorrectness Logic for Quantum Programs
Peng Yan, Hanru Jiang, and Nengkun Yu
(University of Technology Sydney, Australia; BIMSA, China)
Publisher's Version
|
| |
Yang, Sen |
Proc. ACM Program. Lang., vol. 6, issue OOPSLA1: "Coverage-Guided Tensor Compiler ..."
Coverage-Guided Tensor Compiler Fuzzing with Joint IR-Pass Mutation
Jiawei Liu, Yuxiang Wei, Sen Yang, Yinlin Deng, and Lingming Zhang
(University of Illinois at Urbana-Champaign, USA; Tongji University, China; Fudan University, China)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
Yao, Peisen |
Proc. ACM Program. Lang., vol. 6, issue OOPSLA1: "Complexity-Guided Container ..."
Complexity-Guided Container Replacement Synthesis
Chengpeng Wang, Peisen Yao, Wensheng Tang, Qingkai Shi, and Charles Zhang
(Hong Kong University of Science and Technology, China; Ant Group, China)
Publisher's Version
|
| |
Yu, Nengkun |
Proc. ACM Program. Lang., vol. 6, issue OOPSLA1: "On Incorrectness Logic for ..."
On Incorrectness Logic for Quantum Programs
Peng Yan, Hanru Jiang, and Nengkun Yu
(University of Technology Sydney, Australia; BIMSA, China)
Publisher's Version
|
| |
Zdancewic, Steve
|
Proc. ACM Program. Lang., vol. 6, issue OOPSLA1: "C4: Verified Transactional ..."
C4: Verified Transactional Objects
Mohsen Lesani, Li-yao Xia, Anders Kaseorg, Christian J. Bell, Adam Chlipala, Benjamin C. Pierce, and Steve Zdancewic
(University of California at Riverside, USA; University of Pennsylvania, USA; Massachusetts Institute of Technology, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
Zhang, Charles |
Proc. ACM Program. Lang., vol. 6, issue OOPSLA1: "Complexity-Guided Container ..."
Complexity-Guided Container Replacement Synthesis
Chengpeng Wang, Peisen Yao, Wensheng Tang, Qingkai Shi, and Charles Zhang
(Hong Kong University of Science and Technology, China; Ant Group, China)
Publisher's Version
|
| |
Zhang, Lingming |
Proc. ACM Program. Lang., vol. 6, issue OOPSLA1: "Coverage-Guided Tensor Compiler ..."
Coverage-Guided Tensor Compiler Fuzzing with Joint IR-Pass Mutation
Jiawei Liu, Yuxiang Wei, Sen Yang, Yinlin Deng, and Lingming Zhang
(University of Illinois at Urbana-Champaign, USA; Tongji University, China; Fudan University, China)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|
| |
Zhang, Linpeng |
Proc. ACM Program. Lang., vol. 6, issue OOPSLA1: "Quantitative Strongest Post: ..."
Quantitative Strongest Post: A Calculus for Reasoning about the Flow of Quantitative Information
Linpeng Zhang and Benjamin Lucien Kaminski
(University College London, UK; Saarland University, Germany)
Publisher's Version
|
| |
Zhou, Yi |
Proc. ACM Program. Lang., vol. 6, issue OOPSLA1: "Linear Types for Large-Scale ..."
Linear Types for Large-Scale Systems Verification
Jialin Li, Andrea Lattuada, Yi Zhou, Jonathan Cameron, Jon Howell, Bryan Parno, and Chris Hawblitzel
(University of Washington, USA; ETH Zurich, Switzerland; Carnegie Mellon University, USA; VMware Research, USA; Microsoft Research, USA)
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Reusable
|