Algebraic effects and handlers have emerged in the programming languages
community as a convenient, modular abstraction for controlling computational
effects. They have found several applications including concurrent programming,
meta programming, and more recently, probabilistic programming, as part of
Pyro's Poutines library. We investigate the use of effect handlers as a
lightweight abstraction for implementing probabilistic programming languages
(PPLs). We interpret the existing design of Edward2 as an accidental
implementation of an effect-handling mechanism, and extend that design to
support nested, composable transformations. We demonstrate that this enables
straightforward implementation of sophisticated model transformations and
inference algorithms.

more |
pdf
| html
None.

arxivml:
"Effect Handling for Composable Program Transformations in Edward2",
Dave Moore, Maria I． Gorinova
https://t.co/rg5erPlyAl

Memoirs:
Effect Handling for Composable Program Transformations in Edward2. https://t.co/eIlsbadYQF

None.

None.

Sample Sizes : None.

Authors: 2

Total Words: 1958

Unqiue Words: 923

We demonstrate an application of the Futamura Projections to human-computer
interaction, and particularly to staging human-computer dialogs. Specifically,
by providing staging analogs to the classical Futamura Projections, we
demonstrate that the Futamura Projections can be applied to the staging of
human-computer dialogs in addition to the execution of programs.

more |
pdf
| html
None.

arxiv_org:
Staging Human-computer Dialogs: An Application of the Futamura Projections. https://t.co/i08q3ocUZu https://t.co/nNbHIbOgZm

arxivml:
"Staging Human-computer Dialogs: An Application of the Futamura Projections",
Brandon M． Williams, Saverio Perugini
https://t.co/b5fxN7bI3p

arxiv_cscl:
Staging Human-computer Dialogs: An Application of the Futamura Projections https://t.co/zrkG6337co

arxiv_cscl:
Staging Human-computer Dialogs: An Application of the Futamura Projections https://t.co/zrkG63kIAY

ComputerPapers:
Staging Human-computer Dialogs: An Application of the Futamura Projections. https://t.co/R0SMLzGIBf

arxiv_cshc:
Staging Human-computer Dialogs: An Application of the Futamura Projections https://t.co/0H3NqWv6AT

None.

None.

Sample Sizes : None.

Authors: 2

Total Words: 2810

Unqiue Words: 804

Incremental computation has recently been studied using the concepts of
change structures and derivatives of programs, where the derivative of a
function allows updating the output of the function based on a change to its
input.
We generalise change structures to change actions, and study their algebraic
properties. We develop change actions for common structures in computer
science, including directed-complete partial orders and Boolean algebras.
We then show how to compute derivatives of fixpoints. This allows us to
perform incremental evaluation and maintenance of recursively defined functions
with particular application to generalised Datalog programs.
Moreover, unlike previous results, our techniques are modular in that they
are easy to apply both to variants of Datalog and to other programming
languages.

more |
pdf
| html
None.

ComputerPapers:
Fixing Incremental Computation: Derivatives of Fixpoints, and the Recursive Semantics of Datalog. https://t.co/G4aA9vRHrL

None.

None.

Sample Sizes : None.

Authors: 4

Total Words: 16486

Unqiue Words: 3281

We propose a flow-insensitive analysis that prunes out portions of code which
are irrelevant to a specified set of data-flow paths. Our approach is fast and
scalable, in addition to being able to generate a certificate as an audit for
the computed result. We have implemented our technique in a tool called DSlicer
and applied it to a set of 10600 real-world Android applications. Results are
conclusive, we found out that the program code can be significantly reduced by
36% on average with respect to a specified set of data leak paths.

more |
pdf
| html
None.

None.

None.

Sample Sizes : None.

Authors: 1

Total Words: 4183

Unqiue Words: 1425

Proof-carrying-code was proposed as a solution to ensure a trust relationship
between two parties: a (heavyweight) analyzer and a (lightweight) checker. The
analyzer verifies the conformance of a given application to a specified
property and generates a certificate attesting the validity of the analysis
result. It suffices then for the checker just to test the consistency of the
proof instead of constructing it. We set out to study the applicability of this
technique in the context of data- flow analysis. In particular, we want to know
if there is a significant performance difference between the analyzer and the
checker. Therefore, we developed a tool, called DCert, implementing an
inter-procedural context and flow-sensitive data-flow analyzer and checker for
Android. Applying our tool to real-world large applications, we found out that
checking can be up to 8 times faster than verification. This important gain in
time suggests a potential for equipping applications on app stores with
certificates that can be checked on mobile...

more |
pdf
| html
ComputerPapers:
Certificate Enhanced Data-Flow Analysis. https://t.co/N4CPCGDEL7

None.

None.

Sample Sizes : None.

Authors: 1

Total Words: 6732

Unqiue Words: 2104

We propose and study StkTokens: a new calling convention that provably
enforces well-bracketed control flow and local state encapsulation on a
capability machine. The calling convention is based on linear capabilities: a
type of capabilities that are prevented from being duplicated by the hardware.
In addition to designing and formalizing this new calling convention, we also
contribute a new way to formalize and prove that it effectively enforces
well-bracketed control flow and local state encapsulation using what we call a
fully abstract overlay semantics.
This document is a technical report accompanying a paper by the same title
and authors, published at POPL 2019. It contains proofs and details that were
omitted from the paper for space and presentation reasons.

more |
pdf
| html
None.

None.

Sample Sizes : None.

Authors: 3

Total Words: 47171

Unqiue Words: 3589

Our main models of computation (the Turing Machine and the RAM) make
fundamental assumptions about which primitive operations are realizable. The
consensus is that these include logical operations like conjunction,
disjunction and negation, as well as reading and writing to memory locations.
This perspective conforms to a macro-level view of physics and indeed these
operations are realizable using macro-level devices involving thousands of
electrons. This point of view is however incompatible with quantum mechanics,
or even elementary thermodynamics, as both imply that information is a
conserved quantity of physical processes, and hence of primitive computational
operations.
Our aim is to re-develop foundational computational models that embraces the
principle of conservation of information. We first define what conservation of
information means in a computational setting. We emphasize that computations
must be reversible transformations on data. One can think of data as modeled
using topological spaces and programs as modeled...

more |
pdf
| html
HNTweets:
Embracing the Laws of Physics: Three Reversible Models of Computation: https://t.co/92Law8R96K Comments: https://t.co/aYLFpwEAS1

arxiv_org:
Embracing the Laws of Physics: Three Reversible Models of Computation. https://t.co/VzRixLj4Bq https://t.co/RQqHnjM624

Aldana_Angel:
https://t.co/hPIJbhsNIb
Embracing the Laws of Physics: Three Reversible Models of Computation
Jacques Carette, Roshan P. James, Amr Sabry

sigfpe:
One for the to-read list: Embracing the Laws of Physics: Three Reversible Models of Computation
https://t.co/KgRMHc4fri

StephenPiment:
Embracing the Laws of Physics: Three Reversible Models of Computation
(using Curry-Howard)
https://t.co/Vh8Tz6W424

jmsunico:
sn-news: #sw #dev #maths Embracing the Laws of Physics: Three Reversible Models of Computation https://t.co/ElxzDRwG2C

hn_frontpage:
Embracing the Laws of Physics: Three Reversible Models of Computation
L: https://t.co/OJVUK7CPhd
C: https://t.co/z6Hu4842H4

kov4l3nko:
Hmmm... just in time:)[1811.03678] Embracing the Laws of Physics: Three Reversible Models of Computation https://t.co/OM1bq2b06X

andrewfnewman:
"Programs as Reversible Deformations" https://t.co/AHTE3QGsBE something to get into if you're not dealing with JavaScript.

kushnerbomb:
gud paper, much more type theory than I expected https://t.co/VxCs4zEmY0

angsuman:
Embracing the Laws of Physics: Three Reversible Models of Computation https://t.co/mMLEyIFsUZ

arxiv_pop:
2018/11/08 投稿 3位
PL(Programming Languages)
Embracing the Laws of Physics: Three Reversible Models of Computation
https://t.co/tbCIzTj0uD
29 Tweets 11 Retweets 52 Favorites

betterhn50:
51 – Embracing the Laws of Physics: Three Reversible Models of Computation https://t.co/JsPmBCjHtD

24hrcarfinance:
[1811.03678] Embracing the Laws of Physics: Three Reversible Models of Computation https://t.co/JZK6hHy943

QuantumPapers:
Embracing the Laws of Physics: Three Reversible Models of Computation. https://t.co/NNq442eSaD

joshtronic:
Embracing the Laws of Physics: Three Reversible Models of Computation - https://t.co/IF5rLlIQdu

dJdU:
“Embracing the Laws of Physics: Three Reversible Models of Computation”
https://t.co/AkPI6aRpga

hackernewsrobot:
Embracing the Laws of Physics: Three Reversible Models of Computation https://t.co/Atno35U9Mi

Rosenchild:
RT @arxiv_org: Embracing the Laws of Physics: Three Reversible Models of Computation. https://t.co/VzRixLj4Bq https://t.co/RQqHnjM624

jackhidary:
RT @StephenPiment: Embracing the Laws of Physics: Three Reversible Models of Computation
(using Curry-Howard)
https://t.co/Vh8Tz6W424

Juan_A_Lleo:
RT @StephenPiment: Embracing the Laws of Physics: Three Reversible Models of Computation
(using Curry-Howard)
https://t.co/Vh8Tz6W424

paul_snively:
RT @sigfpe: One for the to-read list: Embracing the Laws of Physics: Three Reversible Models of Computation
https://t.co/KgRMHc4fri

PLT_cheater:
RT @sigfpe: One for the to-read list: Embracing the Laws of Physics: Three Reversible Models of Computation
https://t.co/KgRMHc4fri

Priceeqn:
RT @StephenPiment: Embracing the Laws of Physics: Three Reversible Models of Computation
(using Curry-Howard)
https://t.co/Vh8Tz6W424

jjcarett2:
RT @arxiv_cslo: Embracing the Laws of Physics: Three Reversible Models of Computation https://t.co/nGVvjPyTqm

maxsnew:
RT @arxiv_cslo: Embracing the Laws of Physics: Three Reversible Models of Computation https://t.co/nGVvjPyTqm

pauldhoward:
RT @StephenPiment: Embracing the Laws of Physics: Three Reversible Models of Computation
(using Curry-Howard)
https://t.co/Vh8Tz6W424

SandMouth:
RT @arxiv_cslo: Embracing the Laws of Physics: Three Reversible Models of Computation https://t.co/nGVvjPyTqm

shubh_300595:
RT @arxiv_org: Embracing the Laws of Physics: Three Reversible Models of Computation. https://t.co/VzRixLj4Bq https://t.co/RQqHnjM624

None.

None.

Sample Sizes : None.

Authors: 3

Total Words: 16963

Unqiue Words: 4120

Effect systems are lightweight extensions to type systems that can verify a
wide range of important properties with modest developer burden. But our
general understanding of effect systems is limited primarily to systems where
the order of effects is irrelevant. Understanding such systems in terms of a
semilattice of effects grounds understanding of the essential issues, and
provides guidance when designing new effect systems. By contrast, sequential
effect systems --- where the order of effects is important --- lack an
established algebraic characterization.
We derive an algebraic characterization from the shape of prior concrete
sequential effect systems. We present an abstract polymorphic effect system
with singleton effects parameterized by an effect quantale --- an algebraic
structure with well-defined properties that can model a range of existing
sequential effect systems. We define effect quantales, derive useful
properties, and show how they cleanly model a variety of known sequential
effect systems. We show that for...

more |
pdf
| html
None.

None.

None.

Sample Sizes : None.

Authors: 1

Total Words: 25272

Unqiue Words: 5006

Deep learning models with convolutional and recurrent networks are now
ubiquitous and analyze massive amounts of audio, image, video, text and graph
data, with applications in automatic translation, speech-to-text, scene
understanding, ranking user preferences, ad placement, etc. Competing
frameworks for building these networks such as TensorFlow, Chainer, CNTK,
Torch/PyTorch, Caffe1/2, MXNet and Theano, explore different tradeoffs between
usability and expressiveness, research or production orientation and supported
hardware. They operate on a DAG of computational operators, wrapping
high-performance libraries such as CUDNN (for NVIDIA GPUs) or NNPACK (for
various CPUs), and automate memory allocation, synchronization, distribution.
Custom operators are needed where the computation does not fit existing
high-performance library calls, usually at a high engineering cost. This is
frequently required when new operators are invented by researchers: such
operators suffer a severe performance penalty, which limits the pace...

more |
pdf
| html
None.

blackenedgold:
tensor comprehensionの論文が更新されてる
[1802.04730] Tensor Comprehensions: Framework-Agnostic High-Performance Machine Learning Abstractions
https://t.co/a2wrV29MUm

None.

None.

Sample Sizes : [0]

Authors: 9

Total Words: 20260

Unqiue Words: 5992

Modern languages are equipped with static type checking/inference that helps
programmers to keep a clean programming style and to reduce errors. However,
the ever-growing size of programs and their continuous evolution require
building fast and efficient analyzers. A promising solution is incrementality,
so one only re-types those parts of the program that are new or changed, rather
than the entire codebase. We propose an algorithmic schema driving the
definition of an incremental typing algorithm that exploits with no changes to
the existing, standard ones. Ours is a grey-box approach, meaning that just the
shape of the input, that of the results and some domain-specific knowledge are
needed to instantiate our schema. Here, we present the foundations of our
approach and we show it at work to derive three different incremental typing
algorithms. The first two implement type checking and inference for a
functional language. The last one type-checks an imperative language to detect
information flow and non-interference. A...

more |
pdf
| html
None.

Experimental incremental typing for a simple subset of CaML

Stargazers: 1

Subscribers: 2

Subscribers: 2

Forks: 0

Open Issues: 0

Open Issues: 0

None.

Sample Sizes : None.

Authors: 3

Total Words: 9648

Unqiue Words: 1901

Assert is a website where the best academic papers on arXiv (computer science, math, physics), bioRxiv (biology), BITSS (reproducibility), EarthArXiv (earth science), engrXiv (engineering), LawArXiv (law), PsyArXiv (psychology), SocArXiv (social science), and SportRxiv (sport research) bubble to the top each day.

Papers are scored (in real-time) based on how verifiable they are (as determined by their Github repos) and how interesting they are (based on Twitter).

To see top papers, follow us on twitter @assertpub_ (arXiv), @assert_pub (bioRxiv), and @assertpub_dev (everything else).

To see beautiful figures extracted from papers, follow us on Instagram.

*Tracking 57,756 papers.*

Sort results based on if they are interesting or reproducible.

Interesting

Reproducible