Tue 25 Aug 2020 03:15 - 03:30 at ICFP Asia 2 - Asia 2 Chair(s): Alan Jeffrey
Functional programming languages are particularly well-suited for building automated reasoning systems, since (among other reasons) a logical term is well modeled by an inductive type, traversing a term can be implemented generically as a higher-order combinator, and backtracking is dramatically simplified by persistent datastructures. However, existing \emph{pure} functional programming languages all suffer a major limitation in these domains: traversing a term requires time proportional to the tree size of the term as opposed to its graph size. This limitation would be particularly devastating when building automation for interactive theorem provers such as Lean and Coq, for which the exponential blowup of term-tree sizes has proved to be both common and difficult to prevent. All that is needed to recover the optimal scaling is the ability to perform simple operations on the memory addresses of terms, and yet allowing these operations to be used freely would clearly violate the basic premise of referential transparency. We show how to use dependent types to seal the necessary pointer-address manipulations behind pure functional interfaces while requiring only a negligible amount of additional trust. We have implemented our approach for the upcoming version (v4) of Lean, and our approach could be adopted by other languages based on dependent type theory as well.
Mon 24 Aug Times are displayed in time zone: Eastern Time (US & Canada) change
14:30 - 14:45 Talk | Achieving High-Performance the Functional Way - A Functional Pearl on Expressing High-Performance Optimizations as Rewrite Strategies ICFP Program Bastian HagedornUniversity of Münster, Germany, Johannes LenfersUniversity of Münster, Thomas KoehlerUniversity of Glasgow, United Kingdom, Xueying QinUniversity of Glasgow, United Kingdom, Sergei GorlatchUniversity of Münster, Germany, Michel SteuwerThe University of Edinburgh DOI Media Attached | ||
14:45 - 15:00 Talk | Staged Selective Parser Combinators ICFP Program Jamie WillisImperial College London, Nicolas WuImperial College London, UK, Matthew PickeringUniversity of Bristol, UK DOI Media Attached | ||
15:00 - 15:15 Talk | Kindly Bent to Free Us ICFP Program Gabriel RadanneInria, Hannes SaffrichUniversity of Freiburg, Peter ThiemannUniversity of Freiburg, Germany DOI Pre-print Media Attached File Attached | ||
15:15 - 15:30 Talk | Sealing Pointer-Based Optimizations Behind Pure Functions ICFP Program Daniel SelsamMicrosoft Research, Simon HudonCarnegie Mellon University, Leonardo De MouraMicrosoft Research, n.n. DOI Media Attached | ||
15:30 - 15:45 Talk | Effects for Efficiency: Asymptotic Speedup with First-Class Control ICFP Program Daniel HillerströmThe University of Edinburgh, Sam LindleyHeriot-Watt University, UK / The University of Edinburgh, UK, John LongleyThe University of Edinburgh DOI Media Attached | ||
15:45 - 16:00 Talk | Computation Focusing ICFP Program DOI Media Attached | ||
16:00 - 16:15 Talk | Retrofitting Parallelism onto OCamlDistinguished Paper ICFP Program KC SivaramakrishnanIIT Madras, Stephen DolanUniversity of Cambridge, UK, Leo WhiteJane Street, Sadiq JafferOpsian and OCaml Labs, Tom KellyOCaml Labs, Anmol SahooIIT Madras, Sudha ParimalaIIT Madras, Atul DhimanIIT Madras, Anil MadhavapeddyOCaml Labs DOI Media Attached | ||
16:15 - 16:30 Talk | Liquid Information Flow ControlDistinguished Paper ICFP Program Nadia PolikarpovaUniversity of California, San Diego, Deian StefanUniversity of California at San Diego, USA, Jean YangCarnegie Mellon University, Shachar ItzhakyTechnion, Israel, Travis HanceCarnegie Mellon University, Armando Solar-LezamaMassachusetts Institute of Technology, USA DOI Media Attached |
Tue 25 Aug Times are displayed in time zone: Eastern Time (US & Canada) change
02:30 - 02:45 Talk | Achieving High-Performance the Functional Way - A Functional Pearl on Expressing High-Performance Optimizations as Rewrite Strategies ICFP Program Bastian HagedornUniversity of Münster, Germany, Johannes LenfersUniversity of Münster, Thomas KoehlerUniversity of Glasgow, United Kingdom, Xueying QinUniversity of Glasgow, United Kingdom, Sergei GorlatchUniversity of Münster, Germany, Michel SteuwerThe University of Edinburgh DOI Media Attached | ||
02:45 - 03:00 Talk | Staged Selective Parser Combinators ICFP Program Jamie WillisImperial College London, Nicolas WuImperial College London, UK, Matthew PickeringUniversity of Bristol, UK DOI Media Attached | ||
03:00 - 03:15 Talk | Kindly Bent to Free Us ICFP Program Gabriel RadanneInria, Hannes SaffrichUniversity of Freiburg, Peter ThiemannUniversity of Freiburg, Germany DOI Pre-print Media Attached File Attached | ||
03:15 - 03:30 Talk | Sealing Pointer-Based Optimizations Behind Pure Functions ICFP Program Daniel SelsamMicrosoft Research, Simon HudonCarnegie Mellon University, Leonardo De MouraMicrosoft Research, n.n. DOI Media Attached | ||
03:30 - 03:45 Talk | Effects for Efficiency: Asymptotic Speedup with First-Class Control ICFP Program Daniel HillerströmThe University of Edinburgh, Sam LindleyHeriot-Watt University, UK / The University of Edinburgh, UK, John LongleyThe University of Edinburgh DOI Media Attached | ||
03:45 - 04:00 Talk | Computation Focusing ICFP Program DOI Media Attached | ||
04:00 - 04:15 Talk | Retrofitting Parallelism onto OCamlDistinguished Paper ICFP Program KC SivaramakrishnanIIT Madras, Stephen DolanUniversity of Cambridge, UK, Leo WhiteJane Street, Sadiq JafferOpsian and OCaml Labs, Tom KellyOCaml Labs, Anmol SahooIIT Madras, Sudha ParimalaIIT Madras, Atul DhimanIIT Madras, Anil MadhavapeddyOCaml Labs DOI Media Attached | ||
04:15 - 04:30 Talk | Liquid Information Flow ControlDistinguished Paper ICFP Program Nadia PolikarpovaUniversity of California, San Diego, Deian StefanUniversity of California at San Diego, USA, Jean YangCarnegie Mellon University, Shachar ItzhakyTechnion, Israel, Travis HanceCarnegie Mellon University, Armando Solar-LezamaMassachusetts Institute of Technology, USA DOI Media Attached |