Programming Systems Group @ University of Kansas

The Programming Systems Group at the University of Kansas is dedicated to advancing the field of programming languages with the goal of empowering programmers to build reliable, efficient, and maintainable software systems with ease. We use programming language abstractions to design languages, type systems, program analysis, and synthesis techniques to design practical tools towards this goal.

I am hiring graduate and undergraduate students for our group! Here are some reasons why our group and KU might be a great fit. Please send me an email and apply to the graduate program in EECS at KU if you want to join us. If you are already at KU, shoot me an email to set up a meeting.

News

[More …]

Projects

Synthesizing correct programs from lightweight specifications

Automating programming correctly has immense potential to increase programmer productivity. All program synthesis methods take as input some form of specification—a description of the user intent. Most formal methods synthesis rely on sophisticated expertise to provide high-assurance specifications. In contrast, recent LLM-based approaches use ambiguous natural language that cannot be checked for correctness against the output. Can we find a middle-ground that uses some combination of lightweight formal methods, test cases, and LLMs to build practical programming automations with minimal user effort?

Can types help in testing and synthesis of dynamic programs?

Random testing and program synthesis have emerged as complementary software assurance methods to type systems. Types help during program development; synthesis helps by automating some programming effort; and testing helps assure correctness after development. However, most random testing and synthesis tools rely on typed languages—excluding all programmers that use dynamic languages to write software! Recently gradual types have emerged to bring the benefits of typing to dynamic languages. Can we bring the philosophy of gradual typing to synthesis and random testing as well?

Designing reliable cloud servers and APIs

Cloud services ranging from social networking to finance are an important part of our daily life; yet we face regular issues of downtimes, crashes, and even disastrous bugs. A key factor behind the complexity is the web server application state, backed by external and/or distributed databases. Additionally, network flakiness, asynchronous programming, and use of a myriad of external APIs make it difficult to reason about such programs. Can we build tools that aid programmers to build better cloud servers and REST APIs by reasoning about intermittent bugs like idempotency or consensus problems?

People

Publications

Absynthe: Abstract Interpretation-Guided Synthesis
Sankha Narayan Guria, Jeffrey S. Foster, and David Van Horn
PLDI 2023

ANOSY: Approximated Knowledge Synthesis with Refinement Types for Declassification
Sankha Narayan Guria, Niki Vazou, Marco Guarnieri, and James Parker
PLDI 2022

RbSyn: Type- and Effect-Guided Program Synthesis
Sankha Narayan Guria, Jeffrey S. Foster, and David Van Horn
PLDI 2021

Type-Level Computations for Ruby Libraries
Milod Kazerounian, Sankha Narayan Guria, Niki Vazou, Jeffrey S. Foster, and David Van Horn
PLDI 2019