Every week, one person is assigned to give an hour-long (or less) presentation on a topic of their choice.
Occasionally, we receive external speakers.
Drinks and snacks will be served.
|
July 16, 2024
|
Teaching the Art of Functional Programming using Automated Grading
Aliya Hameer (invited speaker)
Paper and slides
Abstract
Online programming platforms have immense potential to improve students’ educational experience. They
make programming more accessible, as no installation is required; and automatic grading facilities provide
students with immediate feedback on their code, allowing them to to fix bugs and address errors in their
understanding right away. However, these graders tend to focus heavily on the functional correctness of a
solution, neglecting other aspects of students’ code and thereby causing students to miss out on a significant
amount of valuable feedback.
In this talk, we recount our experience in using the Learn-OCaml online programming platform to
teach functional programming in a second-year university course on programming languages and paradigms.
Moreover, we explore how to leverage Learn-OCaml’s automated grading infrastructure to make it easy
to write more expressive graders that give students feedback on properties of their code beyond simple
input/output correctness, in order to effectively teach elements of functional programming style. In particular,
we describe our extensions to the Learn-OCaml platform that evaluate students on test quality and code style.
By providing these tools and a suite of our own homework problems and associated graders, we aim to
promote functional programming education, enhance students’ educational experience, and make teaching and
learning typed functional programming more accessible to instructors and students alike, in our community
and beyond.
|
|
July 9, 2024
|
A Gentle Introduction to Session Types
Chuta Sano
Slides
Abstract
Not many people in our research group work on session
types. Let's change that. I will be going over an abridged (and
admittedly biased) history of session types from Honda to a more modern
presentation of session types more closer to linear logic. My hope is to
get the audience's feet wet with session types so that more "up to date"
research on session types can follow!
|
|
July 2, 2024
|
Efficient Evaluation of Lazy Programs, or Compilation of Call-by-Need
Clare Jang
Slides
Abstract
Lazy evaluation is a great tool for constructing a composable program:
it helps us to use parser combinators without messing with recursions. It allows us to keep
the optimal amortised time complexity for persistent data structures. It also opens a way
to use co-data such as a stream. The question is: can we actually enjoy the benefits of lazy
programming without harming real performance? In this talk, I will cover the reason why this
is not trivial and two classic and most influential attempts to solve the issues: G-machine and
Three-Instruction-Machine (TIM). These two show us the key ideas for evaluating and compiling
a lazy program and provide guiding posts for more recent and practical methods
(e.g. Spineless Tagless G-Machine and "Compiling without Continuation")
|
|
June 25, 2024
|
Pure Type Systems
Antoine Gaulin
Slides
Abstract
Pure type systems (PTSs) provide a unified framework for describing type systems for the λ-calculus.
This allows studying large classes of typed λ-calculi simultaneously.
In particular, one can specify properties of type systems, such as predicativity, and prove meta-theoretic results conditional on these properties.
While PTSs can describe a large variety of type systems, the λ-calculus is, on its own, impractical and difficult to use.
A key advantage of PTS is that we can define extensions of the λ-calculus, say with pairs, definitions, etc., independently of the original type system.
With suitable extensions, we obtain a framework capable of describing practical programming languages, including Standard ML.
Moreover, it is possible study the impact of the new features on arbitrary type systems.
In particular, one can define an extension and show that it preserves normalization, indicating that it is a safe extension.
|
|
June 18, 2024
|
A Bidirection Demand Semantics for Mechanized Cost Analysis of Lazy Programs
Maite Kramarz
Abstract
Lazy evaluation is a powerful tool that enables better
compositionality and potentially better performance in functional
programming, but it is challenging to analyze its computation cost.
Existing works either require manually annotating sharing, or rely on
separation logic to reason about heaps of mutable cells. In this talk,
we discuss a bidirectional demand semantics that allows for extrinsic
reasoning about the computation cost of lazy programs without relying on
special program logics. We demonstrate how this semantics can be applied
to both simple sorting algorithms and more complex data structures which
rely on laziness.
|
|
June 11, 2024
|
Yet Another Lecture on Normalization for Type Theory
Jason Hu
Abstract
In this talk, I begin with a less well-known Goedel's Church's paradox to explain why even regular mathematics needs to resolve the halting problem if it carries a notion of computation. For a type theory, the halting problem is resolved by proving normalization, which asserts that all well-typed terms terminate. Continuing Jake's talk on definitional interpreters last week, I give a different normalization algorithm from the one I showed previously.
|
|
June 4, 2024
|
Continuation-Passing Style and Defunctionalization
Jacob Errington
Abstract
Continuation-Passing Style (CPS) and defunctionalization (d17n) are two program transformations that when used in conjunction, witness a duality between imperative and declarative programming. Whereas CPS makes explicit the fine-grained control flow of a program, d17n eliminates higher-order functions. By combining these two transformations, we obtain a general strategy for transforming programs expressed declaratively into imperative programs:
1. convert the given program to CPS by introducing a functional parameter to accumulate pending operations in a stack; and
2. defunctionalize this accumulator to realize it as a first-order stack data structure.
The resulting program takes on imperative qualities: its function calls are akin to gotos as those functions never return, and the parameters of those functions are sometimes akin to mutable variables. In this presentation I will quickly review the CPS transformation before introducing d17n in general. Then, I will explore a piece of functional programming folklore relating these concepts: I will demonstrate the application of the CPS+d17n transformation to a left-to-right, call-by-value interpreter for a lambda calculus, giving rise to a stack-based state transition system that is precisely the CEK machine of Felleisen and Friedman.
|
|
May 28, 2024
|
Type Error Localization
Max Kopinsky
Abstract
Traditional implementations of strongly-typed functional programming languages often miss the root cause of type errors. As a consequence, type error messages are often misleading and confusing - particularly for students learning such a language. We describe Tyro, a type error localization tool which determines the optimal source of an error for ill-typed programs following fundamental ideas by Pavlinovic et al. : we first translate typing constraints into SMT (Satisfiability Modulo Theories) using an intermediate representation which is more readable than the actual SMT encoding; during this phase we apply a new encoding for polymorphic types. Second, we translate our intermediate representation into an actual SMT encoding and take advantage of recent advancements in off-the-shelf SMT solvers to effectively find optimal error sources for ill-typed programs. Our design maintains the separation of heuristic and search also present in prior and similar work. In addition, our architecture design increases modularity, re-usability, and trust in the overall architecture using an intermediate representation to facilitate the safe generation of the SMT encoding. We believe this design principle will apply to many other tools that leverage SMT solvers.
Our experimental evaluation reinforces that the SMT approach finds accurate error sources using both expert-labeled programs and an automated method for larger-scale analysis. Compared to prior work, Tyro lays the basis for large-scale evaluation of error localization techniques, which can be integrated into programming environments and enable us to understand the impact of precise error messages for students in practice.
|
|
May 23, 2024
|
Extending Scala for Safe Concurrent Programming
Phillip Haller (invited speaker)
Abstract
Concurrent programming is notorious for hazards such as data races and
deadlocks. At the same time, program executions are difficult to
reproduce due to various sources of nondeterminism, complicating the
debugging of concurrent programs. These challenges have motivated work
on ensuring safety statically using type systems. Type-based
prevention of data races is a major challenge in the context of
object-oriented programming languages due to pervasive mutation and
aliasing. In addition, extending the type systems of existing
languages is a challenge, preventing recent advances from practical use.
This talk presents LaCasa, a language and type system extending Scala
with uniqueness typing and heap isolation. Goals of the language
extension include (a) integrating with the full Scala language, (b)
minimizing the overhead of type annotations, and (c) enabling the
reuse of existing code without source code changes. We show how LaCasa
prevents data races in concurrent programs based on the actor model.
We then present a variant, Parallel LaCasa, which extends data-race
safety to the Async-Finish model. Finally, we discuss the relation to
|
|
May 21, 2024
|
Code generation on OCaml by LLMs
Jaylene Zhang
Abstract
TBD
|
|
May 14, 2024
|
"Un"-intuitionistic logic
Chuta Sano
Abstract
TBD
|
|
May 7, 2024
|
Polymorphism in Adjoint Foundation of Metaprogramming
Clare Jang
Abstract
TBD
|
|
April 30, 2024
|
Contextual Refinement Types
Antoine Gaulin
Abstract
TBD
|
|
April 23, 2024
|
Dependent Layered Modal Type Theory
Jason Hu
Abstract
TBD
|