Papers We Love @paperswelove@mstdn.io

Combining physical and visual simulation---creation of the planet Jupiter for the film “2010” - Yaeger, et al https://buff.ly/2Qi0T6D

#pwlconf2018 #siggraph1986 #fluiddynamics #animation #fx #film

Stable Fluids by Jos Stam - https://buff.ly/2M9DOQa

#pwlconf2018 #3d #computergraphics #animation #fluids

A Universal Turing Machine with Two Internal States - Claude Shannon

PDF: http://buff.ly/2pOlMrA

#history #compsci #turing

https://mstdn.io/media/yLIIj4OG68qW2X7Xp_s

Reliable Circuits Using Less Reliable Relays - Moore, Shannon

PDF: http://buff.ly/2qjvghI

#history #compsci #electronics

https://mstdn.io/media/zHlCvIB6UMdGDiFVgeM

Communication Theory of Secrecy Systems - Claude Shannon

PDF: http://buff.ly/2qiZOAy

#history #compsci #infosec #crypto

https://mstdn.io/media/A7L1J54wCWpUYhBjVfk

A Mathematical Theory of Communication - Claude Shannon

Link: http://buff.ly/2pBTTrh

#compsci #history #informationtheory

https://mstdn.io/media/0YqU4AW9x3zPdRgbmIc

A Symbolic Analysis of Relay and Switching Circuits - Claude Shannon

PDF: buff.ly/2qjuBNr

#compsci #history #foundations

https://mstdn.io/media/xQt5EIA-aPeW588DH8w

Jia, et al.

PDF: http://buff.ly/2qmFsU9

In this work, we augment a spoken dialogue system with the ability to learn about new concepts by conversing with the user in natural language.

#language #learning

https://mstdn.io/media/RXXojv8nKrs9vP26zxA

Artzi, Zettlemoyer

Link: http://buff.ly/2qeatKF

In this paper, we present an approach for using conversational interactions of this type to induce semantic parsers. We demonstrate learning without any explicit annotation of the meanings of user utterances.

#parser #learning #language https://mstdn.io/media/ZzXROhQBvN-lybzWGrY

Naturalizing a Programming Language via Interactive Learning - Wang, et al.

Link: http://buff.ly/2qmsghU

#machinelearning #language

https://mstdn.io/media/mlFdXpBBBuCSBgHoi24

Backhouse, Hoogendeijk

Link: http://buff.ly/2p2Qu13

The "Boom hierarchy" is a hierarchy of types that begins at the level of trees and includes lists, bags and sets. This hierarchy forms the basis for the calculus of total functions developed by Bird and Meertens, and which has become known as the "BirdMeertens formalism".

#types #programming #formalism

https://mstdn.io/media/6UY8dMXpj8ZuvSYfsF0

Hutton

PDF: buff.ly/2pP3ffE

In functional programming, fold is a standard operator that encapsulates a simple pattern of recursion for processing lists. This article is a tutorial on two key aspects of the fold operator for lists.

#recursion #programming #haskell

https://mstdn.io/media/8N_BtyPSe10Cvcb9kTo

Prequiça, et al

PDF: buff.ly/2oT6qTE

This paper describes Treedoc, a novel CRDT design for cooperative text editing. An essential property is that the identifiers of Treedoc atoms are selected from a dense space.

#CRDT #data #replication #tech #treedoc

https://mstdn.io/media/A5LvF5pox09oZxmxxV0

Letia, Preguiça, Shapiro

PDF: http://buff.ly/2o7dONX

A CRDT is a data type whose operations commute when they are concurrent. Replicas of a CRDT eventually converge without any complex concurrency control. As an existence proof, we exhibit a non-trivial CRDT: a shared edit buffer called Treedoc. We outline the design, implementation and performance of Treedoc.

#CRDT #data #replication #tech

https://mstdn.io/media/bskzRWX_noPy5BkPepY

Shapiro, Preguiça

PDF: http://buff.ly/2oYIQXL

Commuting operations greatly simplify consistency in distributed systems. This paper focuses on designing for commutativity, a topic neglected previously. We show that the replicas of any data type for which concurrent operations commute converges to a correct value, under some simple and standard assumptions

#CRDT #data #replication #tech

https://mstdn.io/media/GdTu0CCEvZsGh6ivPHY

Mullen, Zuniga, Tatlock, Grossman

PDF: buff.ly/2o7iZhe

Transformations over assembly code are common in many compilers. These transformations are also some of the most bug-dense compiler components. Such bugs could be eliminated by formally verifying the compiler, but state-of-theart formally verified compilers like CompCert do not support assembly-level program transformations.

#compiler #assembly #bugs

https://mstdn.io/media/GcFPGHj15wyra7eEuFA

Herman, Meunier

PDF: buff.ly/2oT5BtY

Programs in embedded languages contain invariants that are not automatically detected or enforced by their host language. We show how to use macros to easily implement partial evaluation of embedded interpreters in order to capture invariants encoded in embedded programs.

#analysis #dsl

https://mstdn.io/media/7PM7gcRTPL0rgIlLsWw

Improving Haskell Types with SMT - Diatchki

PDF: http://buff.ly/2oT1qhL

We present a technique for integrating GHC’s type-checker with an SMT solver. The technique was developed to add support for reasoning about type-level functions on natural numbers, and so our implementation uses the theory of linear arithmetic

#haskell #types #solver #constraints

https://mstdn.io/media/D7QITUTY4N1NwUmhhZk

Type Systems as Macros - Chang, Knauth, Greenman

Link: buff.ly/2iOXn2K

We present Turnstile, a metalanguage for creating typed embedded languages. To implement the type system, programmers write type checking rules resembling traditional judgment syntax. To implement the semantics, they incorporate elaborations into these rules. Turnstile critically depends on the idea of linguistic reuse.

#types #macros #language

https://mstdn.io/media/o4SuTu_018Y_gXHdE9o

Type Tailoring - Greenman, Chang, Felleisen

PDF: http://buff.ly/2oT1Kxh

Type tailoring enables programmers to extend the rules of a type system without modifying the compiler. Programmers may thus codify additional knowledge about functions and methods in the form of a library of typing rules, which others may use without imposing any additional burden on their code or work flow

#types #runtime #libraries #elaborator #compsci

https://mstdn.io/media/NSBRvfLf4eDAbWoSB1A