Learning concepts through conversations in spoken dialogue systems Show more
Bootstrapping semantic parsers from conversations Show more
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.
Elements of a Relational Theory of Datatypes Show more
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".
A tutorial on the universality and expressiveness of fold Show more
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.
A commutative replicated data type for cooperative editing Show more
CRDTs: Consistency without concurrency control Show more
Letia, Preguiça, Shapiro
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.
Designing a commutative replicated data type Show more
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
Verified Peephole Optimizations for CompCert Show more
Mullen, Zuniga, Tatlock, Grossman
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.
Improving the Static Analysis of Embedded Languages via Partial Evaluation Show more
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.
Improving Haskell Types with SMT Show more
Improving Haskell Types with SMT - Diatchki
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
Type Systems as Macros Show more
Type Systems as Macros - Chang, Knauth, Greenman
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.
Paper: Type Tailoring Show more
Type Tailoring - Greenman, Chang, Felleisen
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
Compilers: Analysis of Pointers and Structures Show more
Analysis of Pointers and Structures - Chase, Wegman, Zadeck
High-level languages could be optimized significantly if compilers
could determine automatically how pointers and heap allocated structures are used.
Video: Failure Detectors Show more
Kiran Bhattaram (@kiranb) on Failure Detectors
The problem of consensus is central to many distributed systems algorithms. Failure detectors are central to the way we think about consensus algorithms. In a fully asynchronous system, the FLP impossibility result shows that no consensus solution that can tolerate crash failures exists!