Programming Languages

The World model is an existing functional input-output mechanism for event-driven programming. It is used in numerous popular textbooks and curricular settings. The World model conflates two different tasks -- the definition of an event…

Context: Embedded Domain-Specific Languages (EDSLs) are a common and widely used approach to DSLs in various languages, including Haskell and Scala. There are two main implementation techniques for EDSLs: shallow embeddings and deep…

Context: Trait composition has inspired new research in the area of code reuse for object oriented (OO) languages. One of the main advantages of this kind of composition is that it makes possible to separate subtyping from subclassing;…

Multiparty session types (MST) are a well-established type theory that describes the interactive structure of a fixed number of components from a global point of view and type-checks the components through projection of the global type onto…

Context: Meta programming consists for a large part of matching, analyzing, and transforming syntax trees. Many meta programming systems process abstract syntax trees, but this requires intimate knowledge of the structure of the data type…

ParaSail is a language specifically designed to simplify the construction of programs that make full, safe use of parallel hardware even while manipulating potentially irregular data structures. As parallel hardware has proliferated, there…

Context: The term reactivity is popular in two areas of research: programming languages and distributed systems. On one hand, reactive programming is a paradigm which provides programmers with the means to declaratively write event-driven…

Structure editors allow programmers to edit the tree structure of a program directly. This can have cognitive benefits, particularly for novice and end-user programmers. It also simplifies matters for tool designers, because they do not…

One Monad to Prove Them All is a modern fairy tale about curiosity and perseverance, two important properties of a successful PhD student. We follow the PhD student Mona on her adventure of proving properties about Haskell programs in the…

Tierless Web programming languages allow programmers to combine client-side and server-side programming in a single program. Programmers can then define components with both client and server parts and get flexible, efficient and typesafe…

We notice that the type of catch :: c a -> (e -> c a) -> c a operator is a special case of monadic bind operator (>>=) :: m a -> (a -> m b) -> m b, the semantics (surprisingly) matches, and this observation has many interesting…

Pragmas for loop transformations, such as unrolling, are implemented in most mainstream compilers. They are used by application programmers because of their ease of use compared to directly modifying the source code of the relevant loops.…

This paper describes the design and implementation of CRAQL (Composable Repository Analysis and Query Language), a new query language for source code. The growth of source code mining and its applications suggest the need for a query…

Our aim is to statically verify that in a given reactive program, the length of collection variables does not grow beyond a given bound. We propose a scalable type-based technique that checks that each collection variable has a given…

In program algebra, an algebraic theory of single-pass instruction sequences, three congruences on instruction sequences are paid attention to: instruction sequence congruence, structural congruence, and behavioural congruence. Sound and…

We present a new dynamic partial-order reduction method for stateless model checking of concurrent programs. A common approach for exploring program behaviors relies on enumerating the traces of the program, without storing the visited…

Loop scopes have been shown to be a helpful tool in creating sound loop invariant rules which do not require program transformation of the loop body. Here we extend this idea from while-loops to for-loops and also present sound loop…

Modern architectures require applications to make effective use of caches to achieve high performance and hide memory latency. This in turn requires careful consideration of placement of data in memory to exploit spatial locality, leverage…

This paper presents LWeb, a framework for enforcing label-based, information flow policies in database-using web applications. In a nutshell, LWeb marries the LIO Haskell IFC enforcement library with the Yesod web programming framework. The…

Verification of microkernels, device drivers, and crypto routines requires analyses at the binary level. In order to automate these analyses, in the last years several binary analysis platforms have been introduced. These platforms share a…