2024-winter

Speaker	Time ∧ Location	Paper
	Abstract
Eric Bond	March 8th, 4-5pm in 3901 BBB	Polynomial Time and Dependent Types
	I will be presenting Bob Atkey's 2024 POPL paper: Abstract: We combine dependent types with linear type systems that soundly and completely capture polynomial time computation. We explore two systems for capturing polynomial time: one system that disallows construction of iterable data, and one, based on the LFPL system of Martin Hofmann, that controls construction via a payment method. Both of these are extended to full dependent types via Quantitative Type Theory, allowing for arbitrary computation in types alongside guaranteed polynomial time computation in terms. We prove the soundness of the systems using a realisability technique due to Dal Lago and Hofmann. Our long-term goal is to combine the extensional reasoning of type theory with intensional reasoning about the resources intrinsically consumed by programs. This paper is a step along this path, which we hope will lead both to practical systems for reasoning about programs’ resource usage, and to theoretical use as a form of synthetic computational complexity theory.
Johnson He	March 15th, 4-5pm@3901BBB	The groupoid interpretation of type theory (1998)
	This is the extended and slightly more modern version of the historic paper, "The Groupoid Model Refutes Uniqueness of Identity Proofs (1994)", using Categories with Families (CwFs) instead of Categories with Attributes (CwAs). I hope we'll see a more modern notion of model in the reading group soon.
Yuchen Jiang	March 29th, 4-5pm@3901BBB	Continuation-Based Program Transformation Strategies
	I'll present Mitchell Wand's (classic) work on CPS transformation. The topic is mature and well-known, so I'll try my best to make it more entertaining. Abstract: Program transformations often involve the generalization of a function to take additional arguments. It is shown that in many cases such an additional variable arises as a representation of the continuation or global context in which the function is evaluated. By considering continuations, local transformation strategies can take advantage of global knowledge. The general results are followed by two examples: the ɑ-β tree pruning algorithm and an algorithm for the conversion of a propositional formula to conjunctive normal form.
Matthew Keenan	April 5th, 4-5pm@3901 BBB	Holbert: Reading, Writing and Proving in the Browser
	Abstract: This paper presents Holbert a work-in-progress pedagogical proof assistant and online textbook platform, aimed at the educational use-case, specifically for the teaching of programming language theory. Holbert allows proof exercises and rule definitions to be embedded directly in an online textbook, where proofs and rules can be manipulated using a graphical interface. We give an overview of the logical foundations of Holbert, examples of its use, and give an update as to its current implementation status.
June Kim	April 12th, 4-5pm@3901 BBB	Syntax-Guided Synthesis
	The classical formulation of the program-synthesis problem is to find a program that meets a correctness specification given as a logical formula. Recent work on program synthesis and program optimization illustrates many potential benefits of allowing the user to supplement the logical specification with a syntactic template that constrains the space of allowed implementations. Our goal is to identify the core computational problem common to these proposals in a logical framework. The input to the syntax-guided synthesis problem (SyGuS) consists of a background theory, a semantic correctness specification for the desired program given by a logical formula, and a syntactic set of candidate implementations given by a grammar. The computational problem then is to find an implementation from the set of candidate expressions so that it satisfies the specification in the given theory. We describe alternative solution strategies that combine learning, counterexample analysis and constraint solving. We report on prototype implementations, and present experimental results on the set of benchmarks collected as part of the first SyGuS-Comp competition held in July 2014.
Steven Schaefer	April 19th, 4-5pm@3901 BBB	A Model of Type Theory in Simplicial Sets
	In the same vein as Johnson's presentation of how the groupoid model refutes UIP, I'd like to continue going through a historical treament of homotopy type theory (HoTT). Streicher's paper presents simplicial sets --- a notion of spaces --- as a model of type theory. We will investigate this model and role that Voevodsky's univalence axiom plays in it.

2024-spring-summer

Speaker	Time ∧ Location	Paper
	Abstract
Wenxuan Guo	March 10th, 4-5pm@zoom	ProofBlocks
	1. Autogradeable Scaffolding Activities for Learning to Write Proofs Authors: Seth Poulsen, Mahesh Viswanathan, Geoffrey L. Herman, and Matthew West Abstract: This paper presents "Proof Blocks," a novel software tool designed to assist in the education of mathematical proofs by providing a platform where students can engage with proofs through a drag-and-drop interface. This tool automates grading and offers immediate feedback, making it particularly valuable in large classes. 2. Efficiency of Learning from Proof Blocks Versus Writing Proofs Authors: Seth Poulsen, Yael Gertner, Benjamin Cosman, Matthew West, and Geoffrey L. Herman Abstract: This study evaluates the effectiveness of Proof Blocks compared to traditional proof-writing exercises. It focuses on the efficiency and learning gains associated with each method through a controlled study involving students from a discrete mathematics course. 3. Autogenerating Natural Language Proofs for Proof Education Authors: Seth Poulsen, Matthew West, and Talia Ringer Abstract: This research introduces a Coq plugin that generates natural language proofs from formal proofs, aiming to make proof education more accessible and understandable to students, especially beginners. 4. Evaluation of Educational Software Tools in Teaching Proofs Authors: Seth Poulsen, Geoffrey L. Herman, Mahesh Viswanathan, Matthew West Abstract: This paper examines the use of Proof Blocks in exams for a discrete mathematics course, analyzing thousands of student responses. The data indicates that Proof Blocks are easier for students compared to traditional written proofs, yet yield similar insights into student understanding. Surveys also suggest that students find the interface user-friendly and effective in assessing their proof-writing skills.

2023-fall

Speaker	Time ∧ Location	Paper
	Abstract
Yash Gaitonde	10/13 4-5pm@3941 BBB	End-user encounters with lambda abstraction in spreadsheets
	The value of computational abstractions to non-expert end-user programmers is contentious. We study reactions to the lambda function in Microsoft Excel, which enables users to define their own functions using the spreadsheet formula language, through a thematic analysis of nearly 2,700 comments posted on the Reddit, Hacker News, YouTube, and Microsoft Tech Community online forums. We find that computational abstractions are viewed both as helpful and harmful, that users encounter learning and understanding barriers to applying them, and that there are deficiencies and opportunities in tooling such as in formula editing, versioning, reuse and sharing. We find that the introduction of lambda prompts new debate around whether spreadsheets are code, whether writing formulas can be considered programming, and whether spreadsheet users identify themselves as programmers.
Johnson He	10/27 4-5pm@3941 BBB	A type-theoretical alternative to ISWIM, CUCH, OWHY
	Abstract from the paper: The paper (first written in 1969 and circulated privately) concerns the definition, axiomatization, and applications of the hereditarily monotone and continuous functionals generated from the integers and the Booleans (plus “undefined” elements). The system is formulated as a typed system of combinators (or as a typed λ-calculus) with a recursion operator (the least fixed-point operator), and its proof rules are contrasted to a certain extent with those of the untyped λ-calculus. For publication (1993), a new preface has been added, and many bibliographical references and comments in footnotes have been appended.
Steven Shaefer	11/03 4-5pm@3941 BBB	RustBelt: Securing the Foundations of the Rust Programming Language
	TLDR; Some of the first verification of Rust's borrowing semantics. A little outdated now, but instructive. Rust is a new systems programming language that promises to overcome the seemingly fundamental tradeoff between high-level safety guarantees and low-level control over resource management. Unfortunately, none of Rust’s safety claims have been formally proven, and there is good reason to question whether they actually hold. Specifically, Rust employs a strong, ownership-based type system, but then extends the expressive power of this core type system through libraries that internally use unsafe features. In this paper, we give the first formal (and machine-checked) safety proof for a language representing a realistic subset of Rust. Our proof is extensible in the sense that, for each new Rust library that uses unsafe features, we can say what verification condition it must satisfy in order for it to be deemed a safe extension to the language. We have carried out this verification for some of the most important libraries that are used throughout the Rust ecosystem.
Andrew Blinn	11/10 4-5pm@3941 BBB	Rhombus: A New Spin on Macros without All the Parentheses
	Rhombus is a new language that is built on Racket. It offers the same kind of language extensibility as Racket itself, but using conventional (infix) notation. Although Rhombus is far from the first language to support Lisp-style macros without Lisp-style parentheses, Rhombus offers a novel synthesis of macro technology that is practical and expressive. A key element is the use of multiple binding spaces for context-specific sublanguages. For example, expressions and pattern-matching forms can use the same operators with different meanings and without creating conflicts. Context-sensitive bindings, in turn, facilitate a language design that reduces the notational distance between the core language and macro facilities. For example, repetitions can be defined and used in binding and expression contexts generally, which enables a smoother transition from programming to metaprogramming. Finally, since handling static information (such as types) is also a necessary part of growing macros beyond Lisp, Rhombus includes support in its expansion protocol for communicating static information among bindings and expressions. The Rhombus implementation demonstrates that all of these pieces can work together in a coherent and user-friendly language.
Matthew Keenan ∧ Elanor Tang	11/17 4-5pm@3941 BBB	Program Synthesis from Polymorphic Refinement Types
	We present a method for synthesizing recursive functions that provably satisfy a given specification in the form of a polymorphic refinement type. We observe that such specifications are particularly suitable for program synthesis for two reasons. First, they offer a unique combination of expressive power and decidability, which enables automatic verification—and hence synthesis—of nontrivial programs. Second, a type-based specification for a program can often be effectively decomposed into independent specifications for its components, causing the synthesizer to consider fewer component combinations and leading to a combinatorial reduction in the size of the search space. At the core of our synthesis procedure is a new algorithm for refinement type checking, which supports specification decomposition. We have evaluated our prototype implementation on a large set of synthesis problems and found that it exceeds the state of the art in terms of both scalability and usability. The tool was able to synthesize more complex programs than those reported in prior work (several sorting algorithms and operations on balanced search trees), as well as most of the benchmarks tackled by existing synthesizers, often starting from a more concise and intuitive user input.
Informal	12/8 4-5pm@3941 BBB	An Evaluation Semantics for Classical Proofs