Our weekly meeting and talk series, known affectionately as “PL-wonks”, is open to everyone interested in discussing programming languages research happening here at IU. Our talks include original research, experience reports, and tutorials. We also sometimes present papers from the literature that we're interested in.
Unless otherwise noted, PL talks happen every Friday at 4:15pm in Lindley Hall Room 101. All are welcome to attend. We have a tradition of baking cookies and other treats for our meetings.
|Jan 11||Talk Sign-up Meeting|
|Jan 18||Wren Thornton||Formalizing the left-chiastic simply-typed lambda calculus, or: What I did last summer||Cameron Swords|
|Jan 25||POPL - No Talk|
|Feb 1||Chung-chieh Shan||Probabilistic programming and equational reasoning||Aaron Todd|
|Feb 8||Doaa Hassan||A case of Study in Language Based Information Flow Security: RDR Language||Paul Ojanen|
|Feb 15||Amr Sabry||Fractional Types||Aaron Hsu|
|Feb 22||Jason Hemann||Fun with Turing Tarpits||Cameron Swords|
|Mar 1||Eric Holk||GPU Programming in Rust: Implementing High-level Abstractions in a Systems-level Language||Zach Sparks|
|Mar 8||Marco Gaboardi||Linear Dependent Types For Differential Privacy||Edward Amsden|
|Mar 15||Spring Break - No Talk|
|Mar 22||Cancelled - Please visit Catalyst and CS PhD Admits events|
|Mar 29||Chris & Tim Zakian||Enhancing work-stealing runtimes with concurrency||Paul Ojanen|
|Apr 5||Zach Sparks||Boxing for Diamonds: Modal logic and its applications||Andre Kuhlenschmidt|
|Apr 12||Cameron Swords||A Type and Effect System for Contract Monitoring|
|Apr 19||Suresh Jagannathan||Compositional and Lightweight Dependent Type Inference for ML||Chris & Tim Zakian|
|Apr 26||Cancelled - good luck on finals!|
|May 3||Graduation Ceremony - No Talk|
Come to this meeting to sign up for a talk slot and avoid being “volunteered!”
A couple years ago, in order to handle scrambling in Japanese, I introduced a new calculus for the semantic side of CCG derivations. This simple calculus is easy to describe and it can also be used to formalize keyword-arguments in programming languages, to justify notational shorthands in category theory, and numerous other things I keep stumbling upon. The calculus ties together a number of disparate threads in theoretical linguistics, type theory, logic, and category theory; and seems therefore worthy of future study. But one nagging question is: is it a nice place to do work? Does the calculus have the properties we usually desire from computational formalisms, like confluence and strong normalization?
This summer I worked on answering these questions. Some have been answered in the affirmative. Others remain open, due to limitations in our usual techniques for solving them— and perhaps due to limitations in our understanding of the phenomena in question. This talk relays some of that exploration.
Chung-chieh Shan (joint work with Dylan Thurston)
Probabilistic inference is popular in machine learning and cognitive science, but it is applied much less than it could be because most inference programs are written from scratch by hand. Instead, probabilistic models and inference procedures should be written as separate reusable modules. To this end, a promising approach is to transform clear models to fast inference, using equational reasoning based on measure semantics and computer algebra. We show how to calculate conditional distributions by equational reasoning. In particular, we add a `Lebesgue measure' operation to the monadic representation of stochastic experiments.
Recently, a new approach has been developed: the use of programming language techniques for specifying and enforcing end to end information flow security policies, well known as security-typed programming languages or language-based information flow security. In this talk, I will introduce briefly the basic idea of language based information flow security approach. Next I will present a case of study in this approach, the restricted delegation and revocation language (RDRL), a new domain specific security typed programming language for enforcing information flow policies that varies dynamically due to delegation among principals or later revocation. The the design of RDRL will be presented concerning its syntax (illustrated with some motivating examples) as well as its operational and error semantics. Moreover the implementation of RDRL using the language specification formalism ASF+SDF will be presented . Finally I will conclude with some directions for future work.
The Turing tarpit languages Iota and Jot, while of limited practical use, have a number of features that make them interesting subjects of study, including their simplicity and the novel Godel numbering they suggest. I will briefly motivate Godel numbering and combinatory logic, and describe the SKI combinator basis. I will then walk through the development of the X combinator, Iota, and Jot, and describe some of the above properties in more detail. Finally, I will demonstrate an implementation of Jot in miniKanren, and describe directions of future work.
Graphics processing units (GPUs) have the potential to greatly accelerate many applications, yet programming models remain too low level. Many language-based solutions to date have addressed this problem by creating embedded domain-specific languages that compile to CUDA or OpenCL. These targets are meant for human programmers and thus are less than ideal compilation targets. LLVM recently gained a compilation target for PTX, NVIDIA's low-level virtual instruction set for GPUs. This lower-level representation is more expressive than CUDA and OpenCL, making it easier to support advanced language features such as abstract data types or even certain closures. We demonstrate the effectiveness of this approach by extending the Rust programming language with support for GPU kernels. At the most basic level, our extensions provide functionality that is similar to that of CUDA. However, our approach seamlessly integrates with many of Rust's features, making it easy to build a library of ergonomic abstractions for data parallel computing. This approach provides the expressiveness of a high level GPU language like Copperhead or Accelerate, yet also provides the programmer the power needed to create new abstractions when those we have provided are insufficient.
Differential privacy offers a way to answer queries about sensitive information while offering strong, provable privacy guarantees. Several tools have been developed for certifying that a given query is differentially private. In one approach, Reed and Pierce proposed a functional programming language, Fuzz, for writing differentially private queries. Fuzz uses linear types to track sensitivity, as well as a probability monad to express randomized computation; it guarantees that any program that has a certain type is differentially private. Fuzz can successfully verify many useful queries. However, it fails when the analysis depends on values that are not known statically.
We present DFuzz, an extension of Fuzz with a combination of linear indexed types and lightweight dependent types. This combination allows a richer sensitivity analysis that is able to analyze a larger class of queries, including queries whose sensitivity depends on runtime information. As in Fuzz, the differential privacy guarantees follows directly from the soundness theorem for the type system. We demonstrate the enhanced expressivity of DFuzz by certifying differential privacy a broad class of iterative algorithms that could not be typed previously. We conclude by discussing the challenges of DFuzz type checking.
Chris Zakian and Tim Zakian
Parallelism and concurrency are both important to modern programming. Applications need to use multiple cores by exposing independent computations (parallelism), and they also need to perform IO, including blocking operations that require non-deterministically interleaved threads of control (concurrency). Many libraries for parallelism in C++ are now available (TBB, TPL, Cilk), as well as libraries for lightweight user threading (Qthreads), but no existing systems combine these benefits effectively: i.e. allowing full composability of task-spawning and blocking within programs.
In this paper, we argue that the solution is to enhance existing work-stealing parallel runtimes to become lightweight threading systems as well. We demonstrate this approach by extending Intel Cilk Plus with cooperative threading capabilities (blocked computations). Our solution increases the code size of the Cilk runtime by less than five percent, and imposes very low overhead for Cilk programs that do not use concurrency features. The new concurrency features have lower context-switching overhead than Pthreads, and are comparable to other languages supporting user-level threads.
Basic propositional logic can be extended with the ability to reason about different modes of truth. In particular, I will discuss three different modalities: necessity, possibility, and “lax truth” (ie, truth up to an unspecified constraint). Under the Curry-Howard correspondence, these modalities (and simple extensions thereof) can be used to reason about complicated program domains such as staged computation, security, proof search, and distributed systems. In this talk, I will introduce the basics of modal logic, then discuss how it can be applied to type systems in these areas.
Behavioral contracts have long been heralded as a transparent mechanism which can only affect the semantics of programs by detecting contract violations. This claim persists despite several results going back at least five years that point out to the “effectful” nature of contracts. Indeed, in a typical contract system, the predicates embedded in contracts are sliced and diced and scattered around the program to be enforced or not depending on various, apparently unrelated, control and data flow decisions. In addition, practical contract systems allow the contract writer to execute code and explore data structures that would not have otherwise been executed or explored. Previous attempts to address this problem have focused on devising restrictions on contracts to tame their effects. In this paper, we explore an alternative approach that accepts current implementations of practical contract systems “as is.” Technically, we design and implement a contract system in which contracts specify, not just what predicate to check, but also how to check it, along with a type system that tracks which checks have been performed and which have been deferred. The system unifies and subsumes various previous approaches and explains the semantics of realistic contract systems that employ various strategies for enforcing contracts.
Proving interesting and expressive safety properties of first-order programs typically involves generating verification conditions that can be solved by a first-order decision procedure. Higher-order functions make it complicated, however, to infer the necessary path constraints required to do the same for functional programs. In this talk, we consider a solution to this problem that encodes higher-order features into pure first-order logic formula, whose solution can be extracted using a lightweight counterexample guided refinement loop. Our approach extracts initial verification conditions from dependent typing rules derived by a syntactic scan of the program. Specification of higher-order functions are captured via subtyping chains generated from these types by treating such functions as uninterpreted first-order constructs.
Our technique enables inference and compositional verification of useful safety properties for ML programs, additionally provides counterexamples that serve as witnesses of unsound assertions, does not entail a complex translation or encoding of the original source program into a first-order representation, and is fully integrated within the MLton compiler toolchain.
This is joint work with He Zhu.
Strongly-typed functional languages such as Haskell have several advantages as languages for language implementation. In particular, Algebraic Datatypes with pattern-matching present a natural way to write much of the functionality of the compiler or interpreter in an inductive way. Generalized Algebraic Datatypes allow the typing features of the host language to be employed to ensure that transformations of the AST preserve some notion of type soundness on the AST.
A useful pattern in language implementation is “flattening”, where nested expressions in an AST are converted to a spine of let-bindings of AST primitives, whose sub-expressions are variable references brought into scope by the let bindings. I show how to implement a flattening transformation from a typed AST to a new datatype which preserves the type-soundness of the AST while guaranteeing by its structure that no nested expressions are present. This permits the user to write total functions over the AST which are checked for the preservation of AST type-soundness and assume a flattened representation.