Talks

Nataliya Guts - University of Maryland, College Park

Just do it: Simple Monadic Equational Reasoning

Friday, February 24, 2012

3:30 pm

- 4:30 pm

William Gasarch - University of Maryland, College Park

An Application of Ramsey's Theorem to Proving Programs Terminate: An Exposition

Friday, March 2, 2012

3:00 pm

- 4:00 pm

The Essence of Javascript

Stephen Magill

Friday, March 9, 2012

3:00 pm

- 4:00 pm

Kristopher Micinski - University of Maryland, College Park

Automated Analysis of Security-Critical Javascript APIs

Friday, April 6, 2012

11:00 am

-12:00 pm

Thomas and Isil Dillig - College of William & Mary

Precise and Fully-Automatic Verification of Container-Manipulating Programs

Wednesday, April 11, 2012

12:00 pm

- 1:00 pm

PhD Proposal: Knowledge-Based Security

Piotr Mardziel - University of Maryland, College Park

Friday, April 20, 2012

3:00 pm

- 4:00 pm

Kristopher Micinski - University of Maryland, College Park

Temporal Higher-Order Contracts

Friday, April 27, 2012

3:00 pm

- 4:00 pm

Nataliya Guts - University of Maryland, College Park

Cause Clue Clauses: Error Localization using Maximum Satisï¬ability

Monday, April 30, 2012

12:00 pm

- 1:00 pm

PhD Defense: Clear, Correct, and Efficient Dynamic Software Updates

Christopher M. Hayden - University of Maryland, College Park

Friday, May 4, 2012

3:00 pm

- 4:00 pm

Karla Saur - University of Maryland, College Park

MoCFI: A Framework to Mitigate Control-Flow Attacks on Smartphones

Friday, May 18, 2012

3:00 pm

- 4:00 pm

Nataliya Guts - University of Maryland

Polymonads: reasoning and inference

Friday, August 10, 2012

2:00 pm

- 3:00 pm

The Myrmics Memory Allocator: Hierarchical, Message-Passing Allocation for Global Address Spaces

Polyvios Pratikakis - Institute of Computer Science (ICS), Foundation for Research and Technology (FORTH)

Thursday, September 13, 2012

2:00 pm

- 3:00 pm

First PLUM lightning session

PLUM reading group - UMD

Friday, October 12, 2012

11:00 am

-11:45 am

Jinseong Jeon - University of Maryland, College Park

Dr. Android and Mr. Hide: Fine-grained Permissions in Android Applications

Wednesday, February 27, 2013

11:00 am

-12:00 pm

Scaling Formal Verification by Easing the Burden of Proof

Zach Tatlock - University of California, San Diego

Thursday, May 16, 2013

11:00 am

-12:00 pm

When not all bits are equal: incorporating "worth" into information-flow measures

Mario Alvim - UPenn

Thursday, August 8, 2013

11:00 am

-12:00 pm

NetKAT: Semantic Foundations for Networks

Nate Foster - Cornell

Room 1115 Computer Science Instructional Center (CSI)

Monday, September 9, 2013

4:00 pm

- 5:00 pm

CS Department ⋅ CS Research Seminar ⋅ PL Reading Group

End-User Programming and Intelligent Tutoring Systems

Sumit Gulwani - Microsoft Corporation

Tuesday, September 10, 2013

11:00 am

-12:00 pm

Byron Cook - Principal Researcher at Microsoft Research, and Professor at University College London

Beyond Termination

Tuesday, September 17, 2013

11:00 am

-12:00 pm

Suresh Jagannathan - Professor of Computer Science, Purdue University, soon to be a PM at DARPA

Atomicity Refinement for Verified Compilation

Wednesday, October 23, 2013

11:00 am

-12:00 pm

TouchDevelop: Productive Scripting on and for Touch-based Devices and Web Services

Thomas Ball - Microsoft Research

Thursday, November 7, 2013

11:00 am

-12:00 pm

Miryung Kim - University of Texas at Austin

Automation, Analysis, and Reconstruction of Systematic Software Changes

Tuesday, December 10, 2013

11:00 am

-12:00 pm

Shan Lu - University of Wisconsin, Madison

An effect-oriented approach to concurrency-bug detection and recovery

Wednesday, December 18, 2013

11:00 am

-12:00 pm

Neil Toronto - Brigham Young University

Running Probabilistic Programs Backward

Wednesday, February 26, 2014

11:00 am

-12:00 pm

Bor-Yuh Evan Chang - University of Colorado, Boulder

Fissile Type Analysis: Modular Checking of Almost Everywhere Invariants

Monday, April 7, 2014

2:00 pm

- 3:00 pm

Cinquecento and Programming by Debugging

Stephen Magill - IDA/CCS

Monday, April 21, 2014

2:00 pm

- 3:00 pm

David Walker - Professor of Computer Science, Princeton University

The Frenetic Project: Declarative Languages for Programming Networks

Wednesday, September 24, 2014

11:00 am

-12:00 pm

Willard Rafnsson - Chamlers

End-to-End Information-Flow Security for Interactive Systems

Friday, October 10, 2014

1:00 pm

- 2:00 pm

MC2 Conference Room A.V. Williams Building (AVW)

Definitional Interpreters for Higher-Order Programming Languages

David Van Horn - UMD

Friday, December 5, 2014

1:00 pm

- 2:00 pm

Javran Cheng - University of Maryland

Counterexample-Guided Abstraction Refinement for Symbolic Model Checking

Thursday, December 18, 2014

1:15 pm

- 2:15 pm

David Darais - Harvard University

Galois Transformers and Modular Abstract Interpreters

Wednesday, February 18, 2015

1:30 pm

- 2:30 pm

Karthik Pattabiraman - Assistant Professor, ECE, University of British Columbia (UBC)

Good Enough Dependability: A New Paradigm For Dependable Systems Design

Monday, March 2, 2015

1:00 pm

- 2:00 pm

Matthew A Hammer - Computer Science Dept., University of Maryland, College Park

Incremental Computation with Adapton

Monday, March 9, 2015

1:30 pm

- 2:30 pm

Rance Cleaveland - Computer Science Dept., University of Maryland, College Park

Prove If You Can, Test If You Cannot

3:30 pm

- 4:30 pm

Incremental Computation with Adapton

Matthew Hammer - UMD

Monday, March 30, 2015

1:00 pm

- 2:00 pm

Liquid Types (Rondon et. al.)

ThanhVu (Vu) Nguyen - PLUM, UMD CS

Monday, April 6, 2015

1:00 pm

- 2:00 pm

Total Functional Programming (D. A. Turner)

Kris Micinski - PLUM, UMD CS

Friday, April 10, 2015

2:00 pm

- 3:00 pm

Running Probabilistic Programs Backwards

Neil Toronto - UMD

Monday, April 13, 2015

1:00 pm

- 2:00 pm

Hybrid Type Checking (Corman Flanagan)

Brianna Ren - PLUM, UMD CS

Monday, April 20, 2015

1:00 pm

- 2:00 pm

Michael Greenberg - Princeton University

Tracking the Flow of Ideas through the Programming Languages Literature

Monday, April 27, 2015

1:00 pm

- 2:00 pm

A Core Calculus of Dependency (Abadi et. al.)

Matthew Hammer - PLUM, UMD CS

Monday, May 4, 2015

1:00 pm

- 2:00 pm

Relatively Complete Counterexamples for Higher-Order Programs

Phuc Nguyen - PLUM, UMD CS

Tuesday, July 14, 2015

11:00 am

-12:00 pm

Cristian Cadar - Imperial College

Symbolic Execution for Evolving Software

Wednesday, October 14, 2015

3:30 pm

- 4:30 pm

Gradual Typing for Dart

Fabio Strocco - Department of Computer Science, Aarhus University

Wednesday, October 21, 2015

3:30 pm

- 4:30 pm

Galois Transformers and Modular Abstract Interpreters: Reusable Metatheory for Program Analysis

David Darais - PLUM, UMD

Monday, November 2, 2015

10:30 am

-11:30 am

Luis Pina - Imperial College, London

Multi-version execution for efficient dynamic analysis

Monday, November 16, 2015

1:00 pm

- 2:00 pm

Rupak Majumdar - Max Planck Institute for Software Systems

Algorithmic Analysis for Asynchronous Programs

Wednesday, January 27, 2016

11:00 am

-12:00 pm

Viktor Vafeiadis - MPI-SWS

Program verification under weak memory consistency

Wednesday, February 24, 2016

11:00 am

-12:00 pm

Sam Tobin-Hochstadt - Indiana University

Pycket: a tracing JIT for a functional language

Friday, April 8, 2016

1:00 pm

- 2:00 pm

Luis Pina - Imperial College, London

Tedsuto: A General Framework for Testing Dynamic Software Updates

Wednesday, April 20, 2016

11:00 am

-12:00 pm

Thomas Gilray - University of Utah

Static Analysis with Introspective Polyvariance

Monday, April 25, 2016

11:00 am

-12:00 pm

Marco Gaboardi - University at Buffalo, SUNY

Differentially Private Bayesian Programming

Tuesday, April 26, 2016

11:00 am

-12:00 pm

Improving Android's Reliability and Security

Iulian Neamtiu - NJIT

Friday, May 13, 2016

1:30 pm

- 2:30 pm

Peter Thiemann - Universität Freiburg

A Delta for Hybrid Type Checking

Tuesday, September 13, 2016

1:00 pm

- 2:00 pm

Constructive Galois Connections: Taming the Galois Connection Framework for Mechanized Metatheory.

David Darais - University of Maryland

Thursday, September 15, 2016

2:00 pm

- 2:30 pm

Allocation Characterizes Polyvariance (ICFP practice talk)

Thomas Gilray

Christian Skalka - University of Vermont

Thursday, September 29, 2016

11:00 am

-12:00 pm

CS Department ⋅ PL Reading Group ⋅ Security Reading Group

Defense in Depth: A Synthesis of Prospective and Retrospective Security

3100A Computer and Space Sciences Building (CSS)

Friday, October 7, 2016

3:00 pm

- 4:00 pm

PL Reading Group ⋅ QuICS Seminar

Qwire: A Core Language for Quantum Circuits

Jennifer Paykin - U. Penn

Friday, October 14, 2016

11:00 am

-12:00 pm

CS Department ⋅ CS Research Seminar ⋅ PL Reading Group

Programming with Numerical Uncertainties

Eva Darulova - Max Planck Institute for Software Systems

Monday, October 17, 2016

11:00 am

-12:00 pm

Mike Dodds - Lecturer, Department of Computer Science, University of York

Starling: Simpler proofs of concurrent algorithms

Thursday, November 3, 2016

1:00 pm

- 2:00 pm

Liquid Types for Haskell

Niki Vazou - UCSD

Friday, November 18, 2016

1:30 pm

- 2:30 pm

Monitoring and Blame Assignment for Higher-Order Session Types

Anna Gommerstadt - CMU

Monday, February 20, 2017

2:00 pm

- 3:00 pm

Ravi Chugh - University of Chicago

Direct Manipulation Programming Systems

Monday, February 27, 2017

11:00 am

-12:00 pm

Type-Driven Program Synthesis

Nadia Polikarpova - MIT

Friday, March 3, 2017

11:00 am

-12:00 pm

Limin Jia - Carnegie Mellon University

Information Flow Security in Practical Systems

Monday, March 27, 2017

10:00 am

-11:00 am

Arthur Azevedo de Amorim - University of Pennsylvania

A semantic account of metric preservation

Friday, April 14, 2017

11:00 am

-12:00 pm

Phosphor: a dynamic taint analysis tool for Java

Jonathan Bell - GMU

Friday, April 21, 2017

11:00 am

-12:00 pm

Swarat Chaudhuri - Rice University

Learning to Write Code, Automatically

Friday, May 26, 2017

11:00 am

-12:00 pm

Danfeng Zhang - Penn State University

Building Provably Secure Computer Systems against Timing Channels

Thursday, June 15, 2017

2:30 pm

- 3:30 pm

Decomposition Instead of Self-Composition for Proving the Absence of Timing Channels

Paul Gazzillo - Yale University

Monday, June 26, 2017

11:00 am

-12:00 pm

Luís Pina - Imperial College London

A DSL Approach to Reconcile Equivalent Divergent Program Executions

Tuesday, June 27, 2017

1:30 pm

- 2:30 pm

A Scalable and Tunable Adaptive Resolution Parallel I/O Framework

Sidharth Kumar - University of Utah

Daniel Schoepe - Chalmers University of Technology

Monday, July 10, 2017

11:00 am

-12:00 pm

MC2 Seminar ⋅ PL Reading Group

Flexible Information-Flow Control

Monday, July 17, 2017

11:00 am

-12:00 pm

Mayur Naik - University of Pennsylvania

Combining Logical and Probabilistic Reasoning in Program Analysis

Thursday, August 31, 2017

10:00 am

-11:00 am

Crypto Reading Group ⋅ MC2 Seminar ⋅ PL Reading Group ⋅ Security Reading Group

Securing Databases from Probabilistic Inference

Marco Guarnieri - ETH Zurich

Wednesday, September 27, 2017

12:00 pm

- 1:00 pm

QWIRE: A Core Language for Quantum Circuits

Kesha

Wednesday, October 4, 2017

12:00 pm

- 1:00 pm

Toward Full Elasticity in Distributed Static Analysis: The Case of Callgraph Analysis

Mike

Wednesday, October 11, 2017

12:00 pm

- 1:00 pm

Under-Constrained Symbolic Execution

Willem Wyndham

Tuesday, October 17, 2017

12:00 pm

- 1:00 pm

Sergio Mover - University of Colorado Boulder

Dynamic Lifestate Verification of Event-Driven Applications

MC2 A.V. Williams Building (AVW)

Wednesday, October 25, 2017

12:00 pm

- 1:00 pm

Fast and Precise Type Checking for JavaScript

Thomas Gilray - University of Maryland

Wednesday, November 1, 2017

12:00 pm

- 1:00 pm

Inference and Evolution of TypeScript Declaration Files

Brianna Ren

Wednesday, November 8, 2017

12:00 pm

- 1:00 pm

Query Checking for Linear Temporal Logic.

Samuel Huang

Friday, November 17, 2017

12:00 pm

- 1:00 pm

Beyond correct and fast: Inspection Testing

Joachim Breitner - UPenn

Wednesday, November 29, 2017

12:00 pm

- 1:00 pm

Niki Vazou - University of Maryland

Gradual Liquid Types

Wednesday, December 6, 2017

12:00 pm

- 1:00 pm

Bringing the Web up to Speed with WebAssembly

Willem Wyndham - University of Maryland

Monday, January 22, 2018

1:00 pm

- 2:00 pm

Guy Steele: It's Time for a New Old Language

Video of Guy Steele

Monday, January 29, 2018

1:00 pm

- 2:00 pm

Testing before Proving in the Coq Proof Assistant

Leonidas Lampropoulos

Tuesday, January 30, 2018

3:00 pm

- 4:00 pm

Paul Gazzillo - Stevens Institute of Technology

Program Analysis for Security

Friday, February 2, 2018

11:00 am

-12:00 pm

Niki Vazou - University of Maryland, College Park

Liquid Haskell: Usable Type-Driven Program Verification

Monday, February 5, 2018

11:00 am

-12:00 pm

Mechanical Systems as a Programming Language

Mark Fuge - UMD

Friday, February 9, 2018

1:30 pm

- 2:30 pm

Byron Cook - Director, Automated Reasoning Group, Amazon Web Services

Formal reasoning for AWS cloud security

Monday, April 9, 2018

1:00 pm

- 2:00 pm

PLunch: Ian Sweet practice talk for POST.

Ian Sweet - PLUM

Monday, April 16, 2018

1:00 pm

- 2:00 pm

PLunch: Verifying quantitative reliability for programs that execute on unreliable hardware (paper)

Kesha Hietala - PLUM lab

Monday, April 23, 2018

1:00 pm

- 2:00 pm

PLunch: The Sovrin Public Permissioned ledger

Willem Wyndham - PLUM lab

Monday, April 30, 2018

1:00 pm

- 2:00 pm

PLunch: Combining Numerical Optimization with SAT Solving

Sankha Guria - PLUM lab

Monday, May 7, 2018

1:00 pm

- 2:00 pm

SMC: Satisfiability Modulo Convex Programming

Prof Yasser Shoukry - ECE at UMD

Monday, August 13, 2018

11:00 am

-12:00 pm

Quantitative information-flow tracking using symbolic execution and statistically-guided model counting

Stephen McCamant - University of Minnesota

Tuesday, August 14, 2018

11:00 am

-12:00 pm

Michael Pradel - TU Darmstadt

DeepBugs: A Learning Approach to Name-based Bug Detection

Wednesday, September 5, 2018

1:00 pm

- 2:00 pm

PLunch: Deriving a probability density calculator (functional pearl)

Mike Hicks

Thursday, September 6, 2018

10:00 am

-11:00 am

Sanjiva Weerawarana - WSO2

Ballerina: A Modern Programming Language Focused on Integration

2120 A.V. Williams Building (AVW)

Wednesday, September 12, 2018

1:00 pm

- 2:00 pm

PLunch: Linear Haskell: Practical Linearity in a Higher-Order Polymorphic Language

James Parker

Wednesday, September 19, 2018

1:00 pm

- 2:00 pm

PLunch: Haskell Symposium practice talk: Theorem Proving for All

Niki Vazou

Wednesday, September 26, 2018

1:00 pm

- 2:00 pm

PLunch: Repairing Decision-Making Programs Under Uncertainty

Kesha Hietala

Friday, September 28, 2018

11:00 am

-12:00 pm

Derek Dreyer - Max Planck Institute for Software Systems (MPI-SWS)

RustBelt: Logical Foundations for the Future of Safe Systems Programming

Wednesday, October 3, 2018

1:00 pm

- 2:00 pm

PLunch: Program Synthesis using Conflict-Driven Learning

Sankha Guria

Monday, October 8, 2018

1:30 pm

- 2:30 pm

Grigory Fedyukovich - Princeton University

Synthesizing Proofs for Program Verification

Wednesday, October 10, 2018

1:00 pm

- 2:00 pm

PLunch: A data-driven CHC solver

Ben Mariano

Wednesday, October 17, 2018

1:00 pm

- 2:00 pm

PLunch: TrustChain: A Sybil-resistant scalable blockchain

Willem Wyndham

Wednesday, October 24, 2018

1:00 pm

- 2:00 pm

PLunch: RacerD: Compositional Static Race Detection

Ian Sweet

Wednesday, October 31, 2018

1:00 pm

- 2:00 pm

PLunch: Quantum Relational Hoare Logic

Robert Rand

Wednesday, November 7, 2018

1:00 pm

- 2:00 pm

PLunch: A Spectrum of Type Soundness and Performance

Cameron Moy

Wednesday, November 14, 2018

1:00 pm

- 2:00 pm

Daniel Fremont - UC Berkeley

PLunch: Algorithmic Improvisation

Wednesday, December 5, 2018

1:00 pm

- 2:00 pm

PLunch: Collapsing Towers of Interpreters

Phil Nguyen

Friday, January 25, 2019

4:00 pm

- 5:00 pm

Luis Pina - George Mason University

Bridging the Update Gap

Wednesday, February 6, 2019

1:00 pm

- 2:00 pm

PLunch: Vale: Verifying High-Performance Cryptographic Assembly Code

Kesha Hietala

Wednesday, February 13, 2019

1:00 pm

- 2:00 pm

PLunch: FrAngel: Component-Based Synthesis with Control Structures

Ben Mariano

Wednesday, February 27, 2019

1:00 pm

- 2:00 pm

PLunch: Mind the Gap: Analyzing the Performance of WebAssembly vs. Native Code

Willem Wyndham

Wednesday, March 6, 2019

1:00 pm

- 2:00 pm

PLunch: Collapsible Contracts: Fixing a Pathology of Gradual Typing

Cameron Moy

Wednesday, March 13, 2019

1:00 pm

- 2:00 pm

PLunch: Trace Abstraction Modulo Probability

Kesha Hietala - University of Maryland, College Park

Wednesday, March 27, 2019

1:00 pm

- 2:00 pm

PLunch: The Meaning of Memory Safety

Mike Hicks - University of Maryland, College Park

Wednesday, April 3, 2019

2:00 pm

- 3:00 pm

PLunch: MVEDSUa: Higher Availability Dynamic Software Updates via Multi-Version Execution

Luis Pina - George Mason University

Wednesday, April 10, 2019

1:00 pm

- 2:00 pm

5105 Brendan Iribe Center for Computer Science and Engineering (IRB)

PLunch: An Abstract Domain for Certifying Neural Networks

Sankha Guria - University of Maryland, College Park

Wednesday, April 17, 2019

1:00 pm

- 2:00 pm

5237 Brendan Iribe Center for Computer Science and Engineering (IRB)

PLunch: The Derivative of a Regular Type is its Type of One-Hole Contexts

Leo Lampropoulos - University of Maryland, College Park

Wednesday, April 24, 2019

1:00 pm

- 2:00 pm

5237 Brendan Iribe Center for Computer Science and Engineering (IRB)

PLunch: Type Systems as Macros

Cameron Moy - University of Maryland, College Park

Wednesday, May 1, 2019

1:00 pm

- 2:00 pm

5237 Brendan Iribe Center for Computer Science and Engineering (IRB)

PLunch: Verified Quantum Computing

Robert Rand - University of Maryland, College Park

Wednesday, May 8, 2019

1:00 pm

- 2:00 pm

5237 Brendan Iribe Center for Computer Science and Engineering (IRB)

PLunch: Type-and-example-directed program synthesis

Phil Nguyen - University of Maryland, College Park

Monday, May 13, 2019

1:00 pm

- 2:00 pm

4237 Brendan Iribe Center for Computer Science and Engineering (IRB)

SNAPL Practice Talk: Formal Verification vs. Quantum Uncertainty

Mike Hicks - University of Maryland, College Park

Wednesday, May 15, 2019

1:00 pm

- 2:00 pm

5237 Brendan Iribe Center for Computer Science and Engineering (IRB)

PLunch: Who Tests the Testers?

Hasan Touma - University of Maryland, College Park

Tuesday, September 10, 2019

11:00 am

-12:00 pm

PLunch: vZ - An Optimizing SMT Solver

James Parker

IRB 5237

Tuesday, September 17, 2019

11:00 am

-12:00 pm

PLunch: Tait's Method: Termination for STLC

Ian Sweet

IRB 5237

Tuesday, September 24, 2019

11:00 am

-12:00 pm

PLunch: Towards a Compiler for Reals

Kesha Hietala

IRB 5237

Tuesday, October 1, 2019

11:00 am

-12:00 pm

PLunch: What You Needa Know about Yoneda

Yiyun Liu

IRB 5237

Monday, October 7, 2019

11:00 am

-12:00 pm

Aws Albarghouthi - University of Wisconsin

Privacy and Automated Verification

3137 Brendan Iribe Center for Computer Science and Engineering (IRB)

Tuesday, October 8, 2019

11:00 am

-12:00 pm

Curry Howard in Coq

Robert Rand

IRB 5237

Tuesday, October 15, 2019

11:00 am

-12:00 pm

Coverage Guided, Property Based Testing

Leonidas Lampropoulos

IRB 5237

Tuesday, October 22, 2019

11:00 am

-12:00 pm

5237 Brendan Iribe Center for Computer Science and Engineering (IRB)

PLunch: Binders Unbound

Ian Sweet

Tuesday, October 29, 2019

11:00 am

-12:00 pm

5237 Brendan Iribe Center for Computer Science and Engineering (IRB)

PLunch: Verified Lifting of Stencil Computations

Sankha Narayan Guria

Tuesday, November 5, 2019

11:00 am

-12:00 pm

PLunch: A unified approach to solving seven programming problems (functional pearl)

Phil Nguyen

5237 Brendan Iribe Center for Computer Science and Engineering (IRB)

Tuesday, November 12, 2019

11:00 am

-12:00 pm

PLunch: When Good Components Go Bad: Formally Secure Compilation Despite Dynamic Compromise

Michael Hicks

5237 Brendan Iribe Center for Computer Science and Engineering (IRB)

Monday, November 25, 2019

11:00 am

-12:00 pm

3137 Brendan Iribe Center for Computer Science and Engineering (IRB)

Data-Driven Software Maintenance

Na Meng - Virginia Tech

Tuesday, November 26, 2019

11:00 am

-12:00 pm

5237 Brendan Iribe Center for Computer Science and Engineering (IRB)

PLunch: Let Arguments Go First

Yiyun Liu

Tuesday, December 3, 2019

11:00 am

-12:00 pm

5237 Brendan Iribe Center for Computer Science and Engineering (IRB)

PLunch: Sound and Robust Solid Modeling via Exact Real Arithmetic and Continuity

Kesha Hietala

Tuesday, December 10, 2019

11:00 am

-12:00 pm

5237 Brendan Iribe Center for Computer Science and Engineering (IRB)

PLunch: Testing and Verification - A Match Made in Heaven

Leonidas Lampropoulos

Monday, February 3, 2020

12:00 pm

- 1:00 pm

5237 Brendan Iribe Center for Computer Science and Engineering (IRB)

Practice job talk

Robert Rand

Monday, February 10, 2020

12:00 pm

- 1:00 pm

5237 Brendan Iribe Center for Computer Science and Engineering (IRB)

A Probabilistic Separation Logic

Michael Hicks

Monday, February 17, 2020

12:00 pm

- 1:00 pm

Frank Fu - Dalhousie University

Linear dependent types for quantum circuit programming

5105 Brendan Iribe Center for Computer Science and Engineering (IRB)

Wednesday, February 19, 2020

2:00 pm

- 3:00 pm

Darius Blasband - Raincode

Grow your own language: The YAFL story

4105 Brendan Iribe Center for Computer Science and Engineering (IRB)

Monday, February 24, 2020

12:00 pm

- 1:00 pm

5237 Brendan Iribe Center for Computer Science and Engineering (IRB)

PLunch: Interaction Trees: Representing Recursive and Impure Programs in Coq

Kesha Hietala

Monday, March 2, 2020

12:00 pm

- 1:00 pm

5237 Brendan Iribe Center for Computer Science and Engineering (IRB)

PLunch: Proving Data-Poisoning Robustness in Decision Trees

Sankha Narayan Guria

Thursday, March 5, 2020

10:30 am

-11:30 am

5107 Brendan Iribe Center for Computer Science and Engineering (IRB)

Building near-term quantum computers: A computer science perspective

Omar Shehab - IonQ, Inc.

Monday, April 13, 2020

12:00 pm

- 1:00 pm

PLunch: On the Expressive Power of Programming Languages

Ian Sweet

Tuesday, April 14, 2020

10:00 am

-11:00 am

Morpheus+ - A Compiler Verification Framework

Liyi Li - University of Illinois, Urbana-Champaign

Monday, April 20, 2020

12:00 pm

- 1:00 pm

PLunch: Guarded Kleene Algebra with Tests

Robert Rand

Zoom

Monday, April 27, 2020

12:00 pm

- 1:00 pm

PLunch: A tour-de-force in Coq Automation

Leonidas Lampropoulos

Zoom

Monday, May 4, 2020

12:00 pm

- 1:00 pm

Comprehensive formal verification of an OS microkernel

David Miller

Zoom

Monday, May 11, 2020

12:00 pm

- 1:00 pm

PLunch: A Simple Differentiable Programming Language

Ian Sweet

Zoom

Monday, June 8, 2020

12:00 pm

- 1:00 pm

Eric Koskinen - Stevens Institute of Technology

Automatic Commutativity Verification with Differencing Abstractions

Zoom

Thursday, June 11, 2020

12:00 pm

- 1:00 pm

Michael Hicks - University of Maryland

Contesting Secure Software Development

Tuesday, September 1, 2020

4:15 pm

- 5:15 pm

PLUM: "What are you working on?" (Part 1)

PLUM Lab - University of Maryland, College Park

Zoom

Tuesday, September 8, 2020

4:15 pm

- 5:15 pm

PLUM Lab - University of Maryland, College Park

PLUM: "What are you working on?" (Part 2)

Zoom

Tuesday, September 15, 2020

4:15 pm

- 5:00 pm

Ian Sweet - University of Maryland, College Park

PLUM Reading Group: Incorrectness Logic, POPL2020

Zoom

Tuesday, September 22, 2020

4:15 pm

- 5:00 pm

Leonidas Lampropoulos - University of Maryland, College Park

Finger Trees Explained Anew, and Slightly Simplified (Functional Pearl)

Zoom

Tuesday, September 29, 2020

4:15 pm

- 5:15 pm

Shiwei Weng - Johns Hopkins University

Higher-Order Demand-Driven Symbolic Evaluation

Zoom

Tuesday, October 6, 2020

4:15 pm

- 5:15 pm

Aviral Goel - Northeastern University

On the Design, Implementation, and Use of Laziness in R

Zoom

Tuesday, October 13, 2020

4:15 pm

- 5:00 pm

Ian Sweet - University of Maryland, College Park

POPLMark Reloaded: Mechanizing Proofs by Logical Relations

Zoom

Tuesday, October 20, 2020

4:15 pm

- 5:00 pm

Sankha Narayan Guria - University of Maryland, College Park

The Next 700 Compiler Correctness Theorems (Functional Pearl)

Zoom

Tuesday, October 27, 2020

4:15 pm

- 5:00 pm

Parsing with zippers (functional pearl)

Deena Postol - University of Maryland, College Park

Zoom

Tuesday, November 3, 2020

4:15 pm

- 5:00 pm

Henry Blanchette - University of Maryland, College Park

Local Type Inference

Zoom

Tuesday, November 10, 2020

4:15 pm

- 5:00 pm

Dependent Type Systems as Macros

Yiyun Liu - University of Maryland, College Park

Zoom

Tuesday, November 24, 2020

4:15 pm

- 5:00 pm

Abstracting Gradual Typing

Jacob Prinz - University of Maryland, College Park

https://umd.zoom.us/j/98723227318?pwd=K0RJZVZZM1Jhd2laMlg1ajgvUjltQT09

Tuesday, December 1, 2020

4:15 pm

- 5:00 pm

Soft Typing

Temur Saidkhodjaev - University of Maryland, College Park

Zoom

Tuesday, December 8, 2020

4:15 pm

- 5:00 pm

RefinedC: An Extensible Refinement Type System for C Based on Separation Logic Programming

Liyi Li - University of Maryland, College Park

Zoom

Monday, February 8, 2021

12:00 pm

-12:45 pm

A Simple Differentiable Programming Language

Ian Sweet - PLUM Lab

Monday, February 15, 2021

12:00 pm

-12:45 pm

Putting gradual types to work

Temur Saidkhodjaev - PLUM Lab

Zoom

Monday, February 22, 2021

12:00 pm

-12:45 pm

Projection-Based Runtime Assertions for Testing and Debugging Quantum Programs

Kesha Hietala - PLUM Lab

Monday, March 1, 2021

12:00 pm

-12:45 pm

Quantum Lambda Calculus

Mike Hicks - PLUM Lab

Zoom

Monday, March 8, 2021

12:00 pm

-12:45 pm

Sankha Narayan Guria - PLUM Lab

egg: Fast and Extensible Equality Saturation

Monday, March 22, 2021

12:00 pm

-12:45 pm

I am not a Number — I am a Free Variable

Deena Postol - PLUM Lab

Monday, March 29, 2021

12:00 pm

-12:45 pm

Snek: Overloading Python Semantics via Virtualization

Yiyun Liu - PLUM Lab

Monday, April 12, 2021

12:00 pm

-12:45 pm

Mesh: Compacting Memory Management for C/C++ Applications

Temur Saidkhodjaev - PLUM Lab

Monday, April 19, 2021

12:00 pm

-12:45 pm

A Survey of Symbolic Execution Techniques

Yiyun Liu - PLUM Lab

Monday, April 26, 2021

12:00 pm

-12:45 pm

Programming Languages for Secure Multiparty Computation

Ian Sweet - PLUM Lab

Monday, May 10, 2021

12:00 pm

-12:45 pm

RbSyn: Type- and Effect-Guided Program Synthesis

Sankha Guria - PLUM Lab

Monday, September 13, 2021

11:30 am

-12:30 pm

5237 Brendan Iribe Center for Computer Science and Engineering (IRB)

Leibniz equality is isomorphic to Martin-Löf identity, parametrically

Henry Blanchette - UMD

Monday, September 20, 2021

11:30 am

-12:30 pm

5105 Brendan Iribe Center for Computer Science and Engineering (IRB)

A functional quantum programming language

Finn Voichick - UMD

Monday, September 27, 2021

11:30 am

-12:30 pm

Toward a Theory of Programming Language and Reasoning Assistant Design: Minimizing

Michael Coblenz - UMD

5105 Brendan Iribe Center for Computer Science and Engineering (IRB)

Monday, October 4, 2021

11:30 am

-12:30 pm

5105 Brendan Iribe Center for Computer Science and Engineering (IRB)

Viaduct: An Extensible, Optimizing Compiler for Secure Distributed Programs

Ian Sweet - UMD

Monday, October 11, 2021

11:30 am

-12:30 pm

5108 Brendan Iribe Center for Computer Science and Engineering (IRB)

How to Design Co-Programs

Deena Postol - UMD

Monday, October 18, 2021

11:30 am

-12:30 pm

5105 Brendan Iribe Center for Computer Science and Engineering (IRB)

Semantics-based program verifiers for all languages

Liyi Li - UMD

Monday, October 25, 2021

11:30 am

-12:30 pm

5105 Brendan Iribe Center for Computer Science and Engineering (IRB)

A Monad for Deterministic Parallelism

José Manuel Calderón Trilla - UMD

Monday, November 1, 2021

11:30 am

-12:30 pm

5105 Brendan Iribe Center for Computer Science and Engineering (IRB)

Normalization by Evaluation

Jacob Prinz - UMD

Monday, November 8, 2021

11:30 am

-12:30 pm

5105 Brendan Iribe Center for Computer Science and Engineering (IRB)

Practical Partial Evaluation for High-Performance Dynamic Language Runtimes

Benjamin Quiring - UMD

Monday, November 15, 2021

11:30 am

-12:30 pm

5105 Brendan Iribe Center for Computer Science and Engineering (IRB)

Quantum Abstract Interpretation

Le Chang - UMD

Monday, November 22, 2021

11:30 am

-12:30 pm

5105 Brendan Iribe Center for Computer Science and Engineering (IRB)

RUDRA: Finding Memory Safety Bugs in Rust at the Ecosystem Scale

Aaron Eline - UMD

Monday, November 29, 2021

11:30 am

-12:30 pm

Squashing Bugs and Empowering Programmers with User-Centered Programming Language Design

Michael Coblenz - UMD

5105 Brendan Iribe Center for Computer Science and Engineering (IRB)

Monday, February 14, 2022

11:00 am

-12:00 pm

5105 Brendan Iribe Center for Computer Science and Engineering (IRB)

C-Saw: Designing an Embedded Language for Reconfigurable Software Architecture

Henry Zhu - Amazon

Monday, February 21, 2022

11:00 am

-12:00 pm

Nikhil Swamy - Microsoft Research

Proof-oriented Programming for High-assurance Systems

virtual: https://umd.zoom.us/j/93825468763?pwd=UXlYZmVkVndXb1owMkpYb2tOQjZFQT09

Monday, March 14, 2022

11:00 am

-12:00 pm

Michael Greenberg - Stevens Institute of Technology

Formal Support for the POSIX Shell

5105 Brendan Iribe Center for Computer Science and Engineering (IRB)

Monday, March 28, 2022

12:30 pm

- 1:30 pm

Kristopher Micinski - Syracuse University

Scaling Binary Corpus Analysis: Assemblage and Reversi

virtual: https://umd.zoom.us/j/93825468763?pwd=UXlYZmVkVndXb1owMkpYb2tOQjZFQT09

Monday, April 25, 2022

11:00 am

-12:00 pm

Cameron Moy - Northeastern University

Programming with Trace Contracts

5105 Brendan Iribe Center for Computer Science and Engineering (IRB)

Monday, September 26, 2022

11:00 am

-12:00 pm

5105 Brendan Iribe Center for Computer Science and Engineering (IRB)

Semantics-Guided Synthesis

Sankha Narayan Guria

Monday, October 3, 2022

11:00 am

-12:00 pm

Sanjiva Prasad - Dept. of Computer Science and Engineering, IIT Delhi

A Sound Secure Information Flow Type System for LUSTRE

5105 Brendan Iribe Center for Computer Science and Engineering (IRB)

Monday, October 10, 2022

11:00 am

-12:00 pm

5105 Brendan Iribe Center for Computer Science and Engineering (IRB)

The Derivative of a Regular Type is its Type of One-Hole Contexts

Henry Blanchette

Monday, October 17, 2022

11:00 am

-12:00 pm

5105 Brendan Iribe Center for Computer Science and Engineering (IRB)

NJPLS Practice

Ben Quiring; Henry Blanchette and Jacob Prinz

Monday, October 24, 2022

11:00 am

-12:00 pm

5105 Brendan Iribe Center for Computer Science and Engineering (IRB)

Solver-Based Gradual Type Migration

Deena Postol

Monday, November 7, 2022

11:00 am

-12:00 pm

Deriving with Derivatives: Efficient Implementations of Abstract Abstract Machines

Ben Quiring

5105 Brendan Iribe Center for Computer Science and Engineering (IRB)

Monday, February 6, 2023

11:00 am

-12:00 pm

Emanuele D'Osualdo - MPI-SWS

Towards expressive, automatic and scalable software verification

5105 Brendan Iribe Center for Computer Science and Engineering (IRB)

Monday, October 23, 2023

11:00 am

-12:00 pm

Satisfiability Modulo Finite Fields (with applications to compilers to zero-knowledge proofs)

Alex Ozdemir - Stanford in the Center for Automated Reasoning

5105 Brendan Iribe Center for Computer Science and Engineering (IRB)

Thursday, September 11, 2025

12:00 pm

- 1:00 pm

5105 Brendan Iribe Center for Computer Science and Engineering (IRB)

Programming Languages and the No-Cloning Theorem

Finn Voichick - University of Maryland

Thursday, September 18, 2025

12:00 pm

- 1:00 pm

5105 Brendan Iribe Center for Computer Science and Engineering (IRB)

Program Generation with Sized Types

Caspar Popova

Thursday, September 25, 2025

12:00 pm

- 1:00 pm

5105 Brendan Iribe Center for Computer Science and Engineering (IRB)

Cost analysis via types

Sai Divvela

Thursday, October 9, 2025

12:00 pm

- 1:00 pm

5105 Brendan Iribe Center for Computer Science and Engineering (IRB)

Random Testing Databases with SQLancer

Alperen Keles

Thursday, October 16, 2025

12:00 pm

- 1:00 pm

5105 Brendan Iribe Center for Computer Science and Engineering (IRB)

A Monad for Nonconstructivity

Jacob Prinz

Thursday, October 23, 2025

12:00 pm

- 1:00 pm

5105 Brendan Iribe Center for Computer Science and Engineering (IRB)

Syntactic Completions with Material Obligations

Pierce Darragh

Thursday, October 30, 2025

12:00 pm

- 1:00 pm

5105 Brendan Iribe Center for Computer Science and Engineering (IRB)

Quantum Shared Memory

Le Chang

Thursday, November 13, 2025

12:00 pm

- 1:00 pm

5105 Brendan Iribe Center for Computer Science and Engineering (IRB)

Divide-and-Conquer Termination Checking

Henry Blanchette

Thursday, November 20, 2025

12:00 pm

- 1:00 pm

5105 Brendan Iribe Center for Computer Science and Engineering (IRB)

Formal Methods for Randomized Concurrent Algorithms

Noam Zilberstein - Cornell University

Thursday, February 5, 2026

12:30 pm

- 1:30 pm

5105 Brendan Iribe Center for Computer Science and Engineering (IRB)

Specifications are about to rule software

Liam DeVoe - Antithesis

Thursday, February 12, 2026

12:30 pm

- 1:30 pm

5105 Brendan Iribe Center for Computer Science and Engineering (IRB)

Logical Step-Indexed Logical Relations

Deena Postol

Thursday, February 26, 2026

12:30 pm

- 1:30 pm

5105 Brendan Iribe Center for Computer Science and Engineering (IRB)

Simulating Failure: Crash Recovery Systems

Justine Frank

Thursday, March 12, 2026

12:30 pm

- 1:30 pm

5105 Brendan Iribe Center for Computer Science and Engineering (IRB)

Let it Flow: Design and Verify a Compiler for Asynchronous Dataflow

Yi Cai

Thursday, March 26, 2026

12:30 pm

- 1:30 pm

5105 Brendan Iribe Center for Computer Science and Engineering (IRB)

Zeroette: The Essence of Zero-Knowledge Computation

Oliwia Kempinski

Thursday, April 2, 2026

12:30 pm

- 1:30 pm

5105 Brendan Iribe Center for Computer Science and Engineering (IRB)

Circuit Optimization via Gradients and Noise-Aware Compilation

Finn Voichick

Thursday, April 9, 2026

12:30 pm

- 1:30 pm

5105 Brendan Iribe Center for Computer Science and Engineering (IRB)

Testing Theorems, Fully Automatically

Segev Elazar Mittelman

Thursday, April 16, 2026

12:30 pm

- 1:30 pm

Type-Based Techniques for the Design and Correctness of Programming Language Implementations

Benjamin Quiring

5105 Brendan Iribe Center for Computer Science and Engineering (IRB)

Thursday, April 30, 2026

12:30 pm

- 1:30 pm

Samaya: Safe Memory Accesses to Expand Coarse Grain Reconfigurable Array Adoption

Jeremy Sha

5105 Brendan Iribe Center for Computer Science and Engineering (IRB)

Thursday, May 7, 2026

12:30 pm

- 1:30 pm