In the #ECOOP23 paper 'Programming with Purity Reflection: Peaceful Coexistence of Effects, Laziness, and Parallelism,' we present a new programming construct that enables selective lazy and/or parallel evaluation.
In a nutshell, purity reflection enables a higher-order function to inspect the purity of a function argument and to vary its behavior based on this information.
For example, a function like Set.count can use parallel evaluation when given a pure predicate and revert to sequential evaluation when given an impure predicate.
The full paper is available here: https://drops-beta.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2023.18
You can read more about purity reflection in Flix here: https://doc.flix.dev/purity-reflection.html
In a nutshell, purity reflection enables a higher-order function to inspect the purity of a function argument and to vary its behavior based on this information.
For example, a function like Set.count can use parallel evaluation when given a pure predicate and revert to sequential evaluation when given an impure predicate.
The full paper is available here: https://drops-beta.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2023.18
You can read more about purity reflection in Flix here: https://doc.flix.dev/purity-reflection.html
MacoCaml: Staging Composable and Compilable Macros
N. Xie, L. White, O. Nicole, J. Yallop
We introduce MacoCaml, a new design and implementation of compile-time code generation for the OCaml language. MacoCaml features a novel combination of macros with phase separation and quotation-based staging, where macros are considered as compile-time bindings, expression cross evaluation phases using staging annotations, and compile-time evaluation happens inside top-level splices. We provide a theoretical foundation for MacoCaml by formalizing a typed source calculus 𝑚𝑎𝑐𝑜 that supports interleaving typing and compile-time code generation, references with explicit compile-time heaps, and modules. We study various crucial properties including soundness and phase distinction. We have implemented MacoCaml in the OCaml compiler, and ported two substantial existing libraries to validate our implementation.
https://xnning.github.io/papers/icfp23.pdf
N. Xie, L. White, O. Nicole, J. Yallop
We introduce MacoCaml, a new design and implementation of compile-time code generation for the OCaml language. MacoCaml features a novel combination of macros with phase separation and quotation-based staging, where macros are considered as compile-time bindings, expression cross evaluation phases using staging annotations, and compile-time evaluation happens inside top-level splices. We provide a theoretical foundation for MacoCaml by formalizing a typed source calculus 𝑚𝑎𝑐𝑜 that supports interleaving typing and compile-time code generation, references with explicit compile-time heaps, and modules. We study various crucial properties including soundness and phase distinction. We have implemented MacoCaml in the OCaml compiler, and ported two substantial existing libraries to validate our implementation.
https://xnning.github.io/papers/icfp23.pdf
The First Room-Temperature Ambient-Pressure Superconductor
https://arxiv.org/abs/2307.12008
Воспроизведения пока нет, но на данный момент звучит и выглядит достаточно правдоподобно.
https://arxiv.org/abs/2307.12008
Воспроизведения пока нет, но на данный момент звучит и выглядит достаточно правдоподобно.
Forwarded from Web to Album
Looking for some interesting summer reading? JFP has just published the latest batch of PhD abstracts for your reading pleasure, with links to the full dissertations. https://www.cambridge.org/core/journals/journal-of-functional-programming/article/phd-abstracts/A32EE036508B4F3B309230D342DA7C2C source
Cambridge Core
PhD Abstracts | Journal of Functional Programming | Cambridge Core
PhD Abstracts - Volume 33
https://arxiv.org/abs/2308.08347
Continuing WebAssembly with Effect Handlers
L. Phipps-Costin, A. Rossberg, A. Guha, D. Leijen, D. Hillerström, KC Sivaramakrishnan, S. Lindley
Continuing WebAssembly with Effect Handlers
L. Phipps-Costin, A. Rossberg, A. Guha, D. Leijen, D. Hillerström, KC Sivaramakrishnan, S. Lindley
All OOPSLA’23 papers https://2023.splashcon.org/track/splash-2023-oopsla#event-overview
2023.splashcon.org
SPLASH 2023 - OOPSLA - SPLASH 2023
The ACM SIGPLAN International Conference on Systems, Programming, Languages and Applications: Software for Humanity (SPLASH) embraces all aspects of software construction and delivery, to make it the premier conference on the applications of programming languages…
A Grounded Conceptual Model for Ownership Types in Rust
The blogpost: https://blog.brownplt.org/2023/09/17/rust-ownership.html
The paper: https://cs.brown.edu/~sk/Publications/Papers/Published/cgk-grounded-model-rust-ownership/
The blogpost: https://blog.brownplt.org/2023/09/17/rust-ownership.html
The paper: https://cs.brown.edu/~sk/Publications/Papers/Published/cgk-grounded-model-rust-ownership/
blog.brownplt.org
A Grounded Conceptual Model for Ownership Types in Rust
Understanding Random Forests: From Theory to Practice, thesis
G. Louppe
https://arxiv.org/abs/1407.7502
G. Louppe
https://arxiv.org/abs/1407.7502
Grokking as Compression: A Nonlinear Complexity Perspective
Z. Liu, Z. Zhong, M. Tegmark
https://arxiv.org/abs/2310.05918
Z. Liu, Z. Zhong, M. Tegmark
https://arxiv.org/abs/2310.05918
Quotient Haskell, Lightweight Quotient Types for All
B. Hewer, G. Hutton
Subtypes and quotient types are dual type abstractions. However, while subtypes are widely used both explicitly and implicitly, quotient types have not seen much practical use outside of proof assistants. A key difficulty to wider adoption of quotient types lies in the significant burden of proof-obligations that arises from their use. In this article, we address this issue by introducing a class of quotient types for which the proof-obligations are decidable by an SMT solver. We demonstrate this idea in practice by presenting Quotient Haskell, an extension of Liquid Haskell with support for quotient types.
https://www.cs.nott.ac.uk/~pszgmh/quotient-haskell.pdf
B. Hewer, G. Hutton
Subtypes and quotient types are dual type abstractions. However, while subtypes are widely used both explicitly and implicitly, quotient types have not seen much practical use outside of proof assistants. A key difficulty to wider adoption of quotient types lies in the significant burden of proof-obligations that arises from their use. In this article, we address this issue by introducing a class of quotient types for which the proof-obligations are decidable by an SMT solver. We demonstrate this idea in practice by presenting Quotient Haskell, an extension of Liquid Haskell with support for quotient types.
https://www.cs.nott.ac.uk/~pszgmh/quotient-haskell.pdf
Capturing Types
https://dl.acm.org/doi/abs/10.1145/3618003
Type systems usually characterize the shape of values but not their free variables. However, many desirable safety properties
could be guaranteed if one knew the free variables captured by values. We describe
variables are succinctly represented in types, and show it can be used to safely implement efects and efect polymorphism via
scoped capabilities. We discuss how the decision to track captured variables guides key aspects of the calculus, and show that
these ideas can be used to guide the implementation of capture checking in a practical programming language.
https://dl.acm.org/doi/abs/10.1145/3618003
Type systems usually characterize the shape of values but not their free variables. However, many desirable safety properties
could be guaranteed if one knew the free variables captured by values. We describe
CC<:□
, a calculus where such capturedvariables are succinctly represented in types, and show it can be used to safely implement efects and efect polymorphism via
scoped capabilities. We discuss how the decision to track captured variables guides key aspects of the calculus, and show that
CC<:□
admits simple and intuitive types for common data structures and their typical usage patterns. We demonstrate howthese ideas can be used to guide the implementation of capture checking in a practical programming language.
Forwarded from ∫f(x)dx
Пародийная песня "The Telnet Song" за авторством Guy Steele была опубликована в Communications of the ACM в апреле 1984 года:
https://dl.acm.org/doi/pdf/10.1145/358027.1035691
https://dl.acm.org/doi/pdf/10.1145/358027.1035691