School of Computer Science PGR Seminar Bhakti Shah and Yunzhe Yuan

Bhakti Shah will present Imperative Syntax for Dependent Types

Abstract: The syntax of a functional, dependently typed programming language differs significantly from that of a typical imperative language. As a part of our goal to develop a dependent type theory and programming language tailored to imperative programmers, we wish to explore the impact of syntax on comprehensibility and usability of a dependently typed language, specifically for experienced imperative programmers. To this end, we develop a prototypical imperative syntax that can be transformed into an existing dependently typed language, Idris. We develop several transformation algorithms to take imperative constructs such as loops and statements from this syntax to terms that typecheck in Idris, allowing programs to be executed within Idris's ecosystem. In particular, we establish a design pattern to take imperative-style code for bounded numbers, length-indexed lists, and length-indexed matrices into executable, dependently typed programs that enforce type-level boundedness and length constraints, using Views for proof-carrying code in dependently typed languages.

Yunzhe Yuan will present Dependency Parsing with Limited Memory: Recovering Global Structure from Local Windows

Abstract: Dependency parsing identifies grammatical relationships between words in a sentence. Processing complete sentences can be costly when GPU memory is limited. Shorter windows reduce the input size, but can separate words that should be connected and produce conflicting analyses. I present a method for reconstructing a dependency tree for the whole sentence from these local predictions. A learned scorer uses word representations from the windows to rank candidate connections and propose links across window boundaries. Experiments across languages, with both graph-based and generative parsers, show that reconstruction improves short-window accuracy and can approach full-sentence performance in some settings. I also discuss the memory savings and computational costs, and examine the dependencies that remain difficult to recover.