Midwest PL Summit 2023

University of Michigan
October, 6th 2023

The Midwest PL Summit is an informal workshop to foster the exchange of ideas and to promote collaboration among faculty and students in the Greater Midwest area. Anyone interested in programming languages and compilers — including applications to areas such as systems, software engineering, and human-computer interaction — is welcome to attend. Our aim is to have a broad selection of talks and posters about ongoing research and any other topics that may be of interest to the PL community. There will be no formal proceedings, but abstracts and slides will be distributed on the web after the workshop.


8:00-9:00 Breakfast

9:00-9:10 Welcome

Session 1 (Chair: Max New)

  • 9:10-9:30 LAProof: a library of formal proofs of accuracy and correctness for linear algebra programs. Ariel Kellison (Cornell University)
  • 9:30-9:50 HardKAT: An IR for Hardware Accelerator Design Languages. Yonathan Fisseha (University of Michigan)
  • 9:50-10:10 Verifying Indistinguishability of Privacy-Preserving Protocols. Kirby Linvill (University of Colorado, Boulder)
  • 10:10-10:30 VyZX: Formal Verification of a Graphical Language. Adrian Lehmann (University of Chicago)

10:30-11:00 Break

Session 2 (Chair: Cyrus Omar)

  • 11:00-11:20 Building a Proof Assistant. Kuen-Bang Hou (Favonia) (University of Minnesota)
  • 11:20-11:40 Carving out a proof theory from Cedille’s core. Andrew Marmaduke (University of Iowa)
  • 11:40-noon Correctness of Intermittent Executions via Modal Crash Types. Myra Dotzel (Carnegie Mellon University)
  • noon-12:20 Reachability Types with Destructive Effects. Haotian (David) Deng (Purdue University)

12:20-1:30 Lunch

Session 3 (Chair: Xinyu Wang)

  • 1:30-1:50 Filling the Creativity Gaps in Reasoning using Logic Learning. Adithya Murali (University of Illinois, Urbana-Champaign)
  • 1:50-2:10 Formal Methods for Trustworthy Deep Learning. Yuhao Zhang (University of Wisconsin)
  • 2:10-2:30 Abstractly Interpreting Differentiable Programming. Jacob Laurel (University of Illinois, Urbana-Champaign)
  • 2:30-2:50 Type-directed Prompt Construction for LLM-powered Programming Assistants. Andrew Blinn (University of Michigan)

2:50-3:20 Break

Session 4 (Chair: Jean-Baptiste Jeannin)

  • 3:20-3:40 PropCov: Effective Coverage Reporting for Property Tests. Jesse Coultas (University of Illinois, Chicago)
  • 3:40-4:00 Compiling and Controlling Symbolic Execution. Guannan Wei (Purdue University)
  • 4:00-4:20 Hyperproperties for Concurrent Programs and Compiler Optimization. Tzu-Han Hsu (Michigan State University)
  • 4:20-4:40 Coyote: A Compiler for Vectorizing Encrypted Arithmetic Circuits. Raghav Malik (Purdue University)

4:40-6:00 Posters

  • Privacy policies as an afterthought: a policy-agnostic language for oblivious computation. Qianchuan Ye
  • A Two-Level Linear Dependent Type Theory. Qiancheng Fu
  • Optimization of a Gradual Verifier: Lazy evaluation of Iso-recursive Predicates as Equi-recursive at Runtime. Jan-Paul Ramos-Dávila
  • Inferring Data Preconditions from Deep Learning Models for Trustworthy Prediction in Deployment. Shibbir Ahmed
  • Predictive Verification using Intrinsic Definitions of Datastructures. Cody Rivera
  • Automating Program Verification for Frame Logic. Hrishikesh Balakrishnan
  • Languages with Decidable Learning: a Meta-theorem. Paul Krogmeier
  • Securing Smart Contracts with Behavioral Contracts. Danning Xie
  • Are Large Language Models Good at Generating Software Specifications? Yes, but not Quite. Nan Jiang
  • Abductive Program Synthesis. Patrick LaFontaine
  • Vicious Cycles in Distributed Software Systems. Shangshu Qian
  • Flan: An Expressive and Efficient Datalog Compiler for Program Analysis. Supun Abeysinghe
  • Covering All the Bases: Type-Based Verification of Test Input Generators. Zhe Zhou
  • Polymorphic Reachability Types: Tracking Freshness, Aliasing, and Separation in Higher-Order Generic Programs. Guannan Wei
  • Hegel : Component-based Synthesis in Sparse Libraries. Ashish Mishra
  • Java Multi-Version eXecution. David Schwartz
  • RustViz 2: Automatically Visualizing Ownership and Borrowing. Zesen Zhao and Yuxiang Yue and Chen Huang
  • Synchronous Programming with Refinement Types. José Luiz Vargas de Mendonça and Jiawei Chen
  • A formalization of the active corner method for collision avoidance in PVS. Nishant Kheterpal and Elanor Tang
  • SlabCity: Whole-Query Optimization using Program Synthesis. Rui Dong and Jie Liu
  • Arborist: Efficient Synthesis of Web Automation Programs using Context-Aware Observational Equivalence. Xiang Li and Xiangyu Zhou
  • Mitigation of Toxic Communications Among Open Source Software Developers. Jaydeb Sarker


Sep 6th – Deadline for talk submissions (submit here)

Sep 22nd – Registration deadline and deadline for student request for travel support (register here)

Oct 6th – MWPLS workshop


Michigan Union – Kuenzel Room (1st floor)

530 S. State St, Ann Arbor, MI



There is metered parking available in front of the Union on either side of State Street and behind the Union on Thompson Street. There is also a visitor parking lot at 400 Thompson Street (behind the Michigan Union) near the Student Affairs Building.


Registration is free and attendees will be provided with complimentary breakfast, lunch, and coffee breaks, but dinner will be a pay-for-yourself affair.

Nearby Hotels

Hampton Inn Ann Arbor-North

Address: 2300 Green Road Ann Arbor, Michigan 48105 USA

DoubleTree Hotel (link here)

Address: 3600 Plymouth Rd, Ann Arbor, Michigan, 48105, USA

Red Roof Inn (link here)

Address: 3621 Plymouth Road, Ann Arbor MI

Residence Inn (link here)

Address: 3535 Green Ct, Ann Arbor, MI 48105

Graduate Hotel (link here)

Address: 615 East Huron St Ann Arbor, MI 48104 United States


Jean-Baptiste Jeannin Cyrus Omar Max New Xinyu Wang