Top 10 Arxiv Papers Today in Programming Languages


2.064 Mikeys
#1. Effect Handling for Composable Program Transformations in Edward2
Dave Moore, Maria I. Gorinova
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
Figures
None.
Tweets
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
Github
None.
Youtube
None.
Other stats
Sample Sizes : None.
Authors: 2
Total Words: 1958
Unqiue Words: 923

2.037 Mikeys
#2. Staging Human-computer Dialogs: An Application of the Futamura Projections
Brandon M. Williams, Saverio Perugini
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
Figures
None.
Tweets
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
Github
None.
Youtube
None.
Other stats
Sample Sizes : None.
Authors: 2
Total Words: 2810
Unqiue Words: 804

2.004 Mikeys
#3. Fixing Incremental Computation: Derivatives of Fixpoints, and the Recursive Semantics of Datalog
Mario Alvarez-Picallo, Alex Eyers-Taylor, Michael Peyton Jones, Luke Ong
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
Figures
None.
Tweets
ComputerPapers: Fixing Incremental Computation: Derivatives of Fixpoints, and the Recursive Semantics of Datalog. https://t.co/G4aA9vRHrL
Github
None.
Youtube
None.
Other stats
Sample Sizes : None.
Authors: 4
Total Words: 16486
Unqiue Words: 3281

0.0 Mikeys
#4. Data-Flow Guided Slicing
Mohamed Nassim Seghir
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
Figures
None.
Tweets
Github
None.
Youtube
None.
Other stats
Sample Sizes : None.
Authors: 1
Total Words: 4183
Unqiue Words: 1425

0.0 Mikeys
#5. Certificate Enhanced Data-Flow Analysis
Mohamed Nassim Seghir
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
Figures
Tweets
ComputerPapers: Certificate Enhanced Data-Flow Analysis. https://t.co/N4CPCGDEL7
Github
None.
Youtube
None.
Other stats
Sample Sizes : None.
Authors: 1
Total Words: 6732
Unqiue Words: 2104

0.0 Mikeys
#6. StkTokens: Enforcing Well-bracketed Control Flow and Stack Encapsulation using Linear Capabilities - Technical Report with Proofs and Details
Lau Skorstengaard, Dominique Devriese, Lars Birkedal
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
Figures
Tweets
Github
None.
Youtube
None.
Other stats
Sample Sizes : None.
Authors: 3
Total Words: 47171
Unqiue Words: 3589

0.0 Mikeys
#7. Embracing the Laws of Physics: Three Reversible Models of Computation
Jacques Carette, Roshan P. James, Amr Sabry
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
Figures
Tweets
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
Github
None.
Youtube
None.
Other stats
Sample Sizes : None.
Authors: 3
Total Words: 16963
Unqiue Words: 4120

0.0 Mikeys
#8. Polymorphic Iterable Sequential Effect Systems
Colin S. Gordon
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
Figures
None.
Tweets
Github
None.
Youtube
None.
Other stats
Sample Sizes : None.
Authors: 1
Total Words: 25272
Unqiue Words: 5006

0.0 Mikeys
#9. Tensor Comprehensions: Framework-Agnostic High-Performance Machine Learning Abstractions
Nicolas Vasilache, Oleksandr Zinenko, Theodoros Theodoridis, Priya Goyal, Zachary DeVito, William S. Moses, Sven Verdoolaege, Andrew Adams, Albert Cohen
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
Figures
None.
Tweets
blackenedgold: tensor comprehensionの論文が更新されてる [1802.04730] Tensor Comprehensions: Framework-Agnostic High-Performance Machine Learning Abstractions https://t.co/a2wrV29MUm
Github
None.
Youtube
None.
Other stats
Sample Sizes : [0]
Authors: 9
Total Words: 20260
Unqiue Words: 5992

0.0 Mikeys
#10. Using Standard Typing Algorithms Incrementally
Matteo Busi, Pierpaolo Degano, Letterio Galletta
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
Figures
None.
Tweets
Github

Experimental incremental typing for a simple subset of CaML

Repository: incremental-mincaml
User: mcaos
Language: OCaml
Stargazers: 1
Subscribers: 2
Forks: 0
Open Issues: 0
Youtube
None.
Other stats
Sample Sizes : None.
Authors: 3
Total Words: 9648
Unqiue Words: 1901

About

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.

Search
Sort results based on if they are interesting or reproducible.
Interesting
Reproducible
Categories
All
Astrophysics
Cosmology and Nongalactic Astrophysics
Earth and Planetary Astrophysics
Astrophysics of Galaxies
High Energy Astrophysical Phenomena
Instrumentation and Methods for Astrophysics
Solar and Stellar Astrophysics
Condensed Matter
Disordered Systems and Neural Networks
Mesoscale and Nanoscale Physics
Materials Science
Other Condensed Matter
Quantum Gases
Soft Condensed Matter
Statistical Mechanics
Strongly Correlated Electrons
Superconductivity
Computer Science
Artificial Intelligence
Hardware Architecture
Computational Complexity
Computational Engineering, Finance, and Science
Computational Geometry
Computation and Language
Cryptography and Security
Computer Vision and Pattern Recognition
Computers and Society
Databases
Distributed, Parallel, and Cluster Computing
Digital Libraries
Discrete Mathematics
Data Structures and Algorithms
Emerging Technologies
Formal Languages and Automata Theory
General Literature
Graphics
Computer Science and Game Theory
Human-Computer Interaction
Information Retrieval
Information Theory
Machine Learning
Logic in Computer Science
Multiagent Systems
Multimedia
Mathematical Software
Numerical Analysis
Neural and Evolutionary Computing
Networking and Internet Architecture
Other Computer Science
Operating Systems
Performance
Programming Languages
Robotics
Symbolic Computation
Sound
Software Engineering
Social and Information Networks
Systems and Control
Economics
Econometrics
General Economics
Theoretical Economics
Electrical Engineering and Systems Science
Audio and Speech Processing
Image and Video Processing
Signal Processing
General Relativity and Quantum Cosmology
General Relativity and Quantum Cosmology
High Energy Physics - Experiment
High Energy Physics - Experiment
High Energy Physics - Lattice
High Energy Physics - Lattice
High Energy Physics - Phenomenology
High Energy Physics - Phenomenology
High Energy Physics - Theory
High Energy Physics - Theory
Mathematics
Commutative Algebra
Algebraic Geometry
Analysis of PDEs
Algebraic Topology
Classical Analysis and ODEs
Combinatorics
Category Theory
Complex Variables
Differential Geometry
Dynamical Systems
Functional Analysis
General Mathematics
General Topology
Group Theory
Geometric Topology
History and Overview
Information Theory
K-Theory and Homology
Logic
Metric Geometry
Mathematical Physics
Numerical Analysis
Number Theory
Operator Algebras
Optimization and Control
Probability
Quantum Algebra
Rings and Algebras
Representation Theory
Symplectic Geometry
Spectral Theory
Statistics Theory
Mathematical Physics
Mathematical Physics
Nonlinear Sciences
Adaptation and Self-Organizing Systems
Chaotic Dynamics
Cellular Automata and Lattice Gases
Pattern Formation and Solitons
Exactly Solvable and Integrable Systems
Nuclear Experiment
Nuclear Experiment
Nuclear Theory
Nuclear Theory
Physics
Accelerator Physics
Atmospheric and Oceanic Physics
Applied Physics
Atomic and Molecular Clusters
Atomic Physics
Biological Physics
Chemical Physics
Classical Physics
Computational Physics
Data Analysis, Statistics and Probability
Physics Education
Fluid Dynamics
General Physics
Geophysics
History and Philosophy of Physics
Instrumentation and Detectors
Medical Physics
Optics
Plasma Physics
Popular Physics
Physics and Society
Space Physics
Quantitative Biology
Biomolecules
Cell Behavior
Genomics
Molecular Networks
Neurons and Cognition
Other Quantitative Biology
Populations and Evolution
Quantitative Methods
Subcellular Processes
Tissues and Organs
Quantitative Finance
Computational Finance
Economics
General Finance
Mathematical Finance
Portfolio Management
Pricing of Securities
Risk Management
Statistical Finance
Trading and Market Microstructure
Quantum Physics
Quantum Physics
Statistics
Applications
Computation
Methodology
Machine Learning
Other Statistics
Statistics Theory
Feedback
Online
Stats
Tracking 57,756 papers.