Principles of Programming Seminar

      Spring 2014

                         May 8th, 2014Brigitte Pientka
Associate Professor in the School of Computer Science at McGill University, Montreal, Canada
Programming Proofs in Context
Host: Frank Pfenning
2:00 PM, Gates-Hillman Center- 8102
                        May 2nd, 2014Stefan Muller
PhD Student in the Computer Science Department- CMU
Expressive and Efficient Functional Semantics for Interaction
Host: Umut Acar
1:30 PM, Gates-Hillman Center- 6501
                         May 1st, 2014Nicolas Feltman
PhD Student in the Computer Science Department- CMU
Creating Data Structures from Algorithms by Stage-splitting a Modal Language
Host: Umut Acar
3:00 PM, Gates-Hillman Center- 6501
                      April 25th, 2014Swarat Chaudhuri
Assistant Professor of Computer Science at Rice University
Adventures in Automated Programming
Host: Umut Acar
1:30 PM, Gates-Hillman Center- 6501
                      April 24th, 2014Alex Aiken
Alcatel-Lucent Professor of Computer Science -- Stanford
Programming Distributed Heterogeneous Architectures with Logical Regions
Host: Kayvon Fatahalian
1:00 PM, Gates-Hillman Center- 4405
                      April 23rd, 2014Evan Chang
Assistant Professor of Computer Science at the University of Colorado Boulder
Fissile Type Analysis: Modular Checking of Almost Everywhere Invariants
Host: Karl Crary
1:30 PM, Gates-Hillman Center- 6501
                February 28th, 2014Cody Roux
Associate Adjunct Professor -- CMU Philosophy Department.
The Structural Theory of Pure Type Systems
Host: Bob Harper
1:30 PM, Gates-Hillman Center- 6501
                February 24th, 2014Michael Greenberg
Post Doc -- Princeton University
Space-Efficient Manifest Contracts
Host: Frank Pfenning
1:30 PM, Gates-Hillman Center- 8102
                 January 23rd, 2014David Spivak
Research Scientist -- MIT
Toward a Categorical Foundation of Functional Reactive Programming
Host: Bob Harper
2:00 PM, Gates-Hillman Center- 6501

          Fall 2013

                November 25, 2013Andrew Sogokon
Research Postgraduate Student -- University of Edinburgh, United Kingdom
Positive Invariance In Safety Verification
Host: Andre Platzer
1:00 PM, Gates-Hillman Center- 6501
                 November 19, 2013Limin Jia
Assistant Research Professor -- CMU ECE & INI
Proving Trace Properties of Programs that Execute Adversary-supplied Code
Host: Umut Acar
3:30 PM, Gates-Hillman Center- 6501

Spring 2013




April 5, 2013
Marcus Völp
Technische Universitat Dresden - Computer Science Department
Why Operating-System Developers Write Barbaric Code and How to Verify It None the Less.
Host: Andre Platzer
2:00 PM. Gates-Hillman Center - 6501
May 2, 2013 Sebastian Erdweg - Post Doc
Technische Universitaet Darmstadt - Software Technology Group
Modular and Automated Type-Soundness Verification for Language Extensions
Host: Christian Kastner - CMU/ISR
1:30 PM, Gates-Hillman - 6501

Fall 2012

October 22, 2012 Susmit Sarkar
University of Cambridge - Computer Laboratory
From C/C++11 to Power and ARM: What is Shared-Memory Concurrency Anyway?
Host: Karl Crary
3:30 PM, Gates-Hillman Center - 4405
October 29, 2012 Marco Gaboardi
University of Pennsylvania, Department of Computer and Information Science
Linear Dependent Types for Differential Privacy
Host: Frank Pfenning
2:00 PM, Gates-Hillman Center - 6115
November 16, 2012 Rustan Leino - Principal Researcher
Microsoft Research, Research in Software Engineering
Induction, Co-induction, Calculations - What's Not to Like About Dafny?
Host: Jonathan Aldrich
2:00 PM, Gates-Hillman Center - 8102
December 4, 2012 Yaron Minsky
Jane Street - Technology Group
The Seven Implementations of Incremental
Host: Umut Acar/Bob Harper
2:00 PM, Gates-Hillman Center - 4405
December 7, 2012 Luis Cairer
Universidade Nova, Lisbon, Portugal
The Type Discipline fo Behavioral Separation
Host: Frank Pfenning
2:00 PM, Gates-Hillman Center - 7501

2011

2011 POP Seminars info - updates pending

2010

2010 POP Seminars info - updates pending

Fall 2009

Remaining Fall 2009 Seminars info - updates pending
Sepember 11, 2009
Ronald Garcia
Computing Innovation Fellow, Carnegie Mellon University
Lazy Evaluation and Delimited Control
3:30 p.m., Gates & Hillman Centers 9115

Summer 2009

Remaining Summer 2009 Seminars info - updates pending
August 7, 2009
K. Subrmani
West Virginia University
A Combinatorial Algorithm for Horn Programs
3:30 p.m., Wean Hall 8220

Spring 2009


January 28, 2009
Walid Taha
Rice University
Programming Languages and the World
3:30 p.m., Wean Hall 8220
February 6, 2009 Umut Acar
Toyota Technological Institute and the University of Chicago
Self-Adjusting Computation in C
3:30 p.m., Wean Hall 8220
February 25, 2009 Luís Caires
Universidade Nova de Lisboa
Dynamic Control of Interference with Spatial-Behavioral Types
3:30 p.m., Wean Hall 8220
March 20, 2009 Dana Scott
Carnegie Mellon University
Semilattices and Domains
3:30 p.m., Wean Hall 4615A
March 27, 2009 Harvey Friedman
Ohio State University
Decision Problems in Strings and Formal Methods
3:30 p.m., Wean Hall 4623
Joint Algorithms/POP Seminar
April 17, 2009

Paul-André Milliès
Universitè Paris VII
Game Semantics in String Diagrams
12:00 p.m., Wean Hall 4615A

May 22, 2009
Derek Dreyer
MPI-SWS
Logical Step-Indexed Logical Relations
3:30 p.m., Wean Hall 8220
May 26, 2009
Peter O'Hearn
Queen Mary, University of London
On the Relation between Session Types and Concurrent Separation Logic
3:30 p.m., Wean Hall 4623
May 27, 2009
Peter Sestoft
IT University of Copenhagen
Fast Sheet-Defined Functions in Spreadsheets
3:30 p.m., Wean Hall 8220


Fall 2008


November 14, 2008 K.Subramani
West Virginia University
Optimal length resolution refutation for difference constraints
3:30 p.m., Wean Hall 8220


Summer 2008


June 13, 2008 Paul Levy
University of Birmingham
Nondeterminism: many questions and (maybe) some answers
3:30 p.m., Wean Hall 8220
June 18, 2008 Paul Levy
University of Birmingham
Call-by-push-value
3:30 p.m., Wean Hall 8220
July 2, 2008 Dino Distefano
Queen Mary, University of London
Compositional Shape Analysis
2:30 p.m., Wean Hall 8220


Spring 2008


January 16, 2008 Derek Dreyer
Max Planck Institute for Software Systems
Mixin' Up the ML Module System
3:30 p.m., Wean Hall 8220
January 18, 2008 Andreas Rossberg
Max Planck Institute for Software Systems
Typed Open Programming -- A higher-order typed approach to dynamic modularity
3:30 p.m., Wean Hall 8220
January 30, 2008 Harry Mairson
Brandeis University
Linear Logic and the Complexity of Control Flow Analysis
2:00 p.m., PPB 300
February 7, 2008
Yitzhak Mandelbaum
AT&T Labs - Research
Formatted Data Considered Harmful
3:30 p.m., Wean Hall 5409

April 18, 2008
Matthew Fluet
Toyota Technological Institute at Chicago
Manticore: A heterogeneous parallel language
3:30 p.m., Wean Hall 8220
        April 23, 2008 Philippa Gardner 
Imperial College
Local Hoare Reasoning about DOM
3:30 p.m., Wean Hall 8220
        April 24, 2008 James Cheney 
University of Edinburgh
Data provenance as dependency analysis
3:30 p.m., Wean Hall 7220
        April 30, 2008 Chris Hawblizel 
Microsoft Research
Typed Assembly Language from an Optimizing Compiler
3:30 p.m., Wean Hall 8220


Fall 2007


October 10, 2007

Vijay Saraswat
IBM TJ Watson Research Center
X10: Concurrent Programming for Modern Architectures
3:30 p.m., Wean Hall 8220

November 28, 2007

Todd Millstein
University of California Los Angeles
Toward Programmer-Defined Effect Systems
3:30 p.m., Wean Hall 8220





Spring 2007


March 2, 2007
Radu Rugina
Cornell University
Practical Shape Analysis
3:30 p.m., Wean Hall 8220
April 6, 2007
Andrej Bauer
How to Connect the Theory and Practice of Computable Mathematics
3:30 p.m., Wean Hall 8220
April 27, 2007 Benjamin C. Pierce
Resourceful Lenses for Ordered Data
3:30 p.m., Wean Hall 8220

May 4, 2007 Brigitte Pientka
Functional Programming with HOAS
3:30 p.m., Wean Hall 8220
May 31, 2007
Luca Cardelli
Artificial Biochemistry
3:30 p.m., Newell-Simon Hall 1305 (Mauldin Auditorium)




Fall 2006


October 5, 2006 Jeff Foster
University of Maryland

Checking Type Safety of Foreign Function Calls
12:00 p.m., Newell-Simon Hall 3305
October 25, 2006 Lars Birkedal
IT University of Copenhagen

Relational Reasoning for Recursive Types and References
3:30 p.m., Wean Hall 8220
December 8, 2006 Kevin Watkins
Abstract interpretation using laziness: proving Conway's Lost
Cosmological Theorem
3:30 p.m., Wean Hall 8220
December 13, 2006 Donna Malayeri
Combining Structural Subtyping and External Dispatch
3:30 p.m., Wean Hall 8220




Spring 2006


April 21, 2006 Jayadev Misra
University of Texas at Austin

A Language for Task Orchestration and its Semantic Properties
3:30 p.m., Wean Hall 8220
May 1, 2006 David Tarditi
Microsoft Research

An Overview of the Singularity Project
3:30 p.m., Newell-Simon Hall 1305 (Mauldin Auditorium)
May 30, 2006
David Walker
Princeton University
PADS/ML: A Functional Data Description Language
3:30 p.m., Wean Hall 8220




Fall 2005


September 30, 2005 Stephen Brookes
Carnegie Mellon Universit
y
A Grainless Semantics for Parallel Programs with Shared Mutable Data
3:30 p.m., Wean Hall 5409
October 7, 2005 Jan Vitek
Purdue Universit
y
Preemptible Atomic Regions
3:30 p.m., Wean Hall 8220
October 28, 2005
Tobias Nipkow
Technische Universität München

A Machine-Checked Model for a Java-Like Language, Virtual Machine and Compiler
3:30 p.m., Wean Hall 8220
November 11, 2005
Christian Urban
Mathematisches Institut der LMU
Nominal Techniques in Isabelle/HOL
2:00 p.m., Wean Hall 7220

December 14, 2005 Patricia Johann
Rutgers University
Parametric Polymorphism, Observational Equivalence, and Monadic Computation
3:30 p.m., Wean Hall 8220




Spring 2005


January 26, 2005
Dan Grossman
University of Washington
Quantified Types in a Safe C-Level Language
3:30 p.m., Wean Hall 8220
March 15, 2005
Harry Mairson
Brandeis University
Constructive Classical Logic
3:30 p.m., Wean Hall 4623

April 1, 2005
Greg Morrisett
Harvard University
Simplifying Regions
3:30 p.m., Wean Hall 8220
May 3, 2005 Norman Ramsey
Harvard University
Choosing Abstractions and Interfaces for Programming-Language Infrastructure
3:30 p.m., Newell-Simon Hall 1305 (Mauldin Auditorium)
May 11, 2005
Yukiyoshi Kameyama
Visiting Scholar, Carnegie Mellon University
on leave from University of Tsukuba
Axiomatizing Delimited Continuations
3:30 p.m., Wean Hall 8220

Summer 2005

July 13, 2005
Frank Pfenning
Carnegie Mellon University
Constructive Authorization Logics
(joint work with Deepak Garg and Kevin Watkins)
3:30 p.m., Wean Hall 8220




Fall 2004


October 4, 2004
Cesare Tinelli
3:30 p.m., Wean Hall 4623
October 29, 2004
Simon Peyton Jones
3:30 p.m., Wean Hall 8220
November 15, 2004
Barry Jay
University of Technology, Sydney
The Pattern Calculus

3:30 p.m., Wean Hall 4623




Summer 2004


June 14, 2004
Robert O'Callahan
IBM TJ Watson Research Center
(joint work with Simon Goldsmith and Alex Aiken)
3:30 p.m., Wean Hall 8220
June 28, 2004
Andrew Pitts
University of Cambridge Computer Laboratory
Equivariant Semantics
3:30 p.m., Wean Hall 4623
July 21, 2004 Michael Hicks
University of Maryland, College Park
Mutatis Mutandis: Safe and Predictable Dynamic Software Updating
3:30 p.m., Wean Hall 8220





Spring 2004


January 23, 2004
Jonathan Aldrich
Carnegie Mellon University
Ownership Domains: High-level Reasoning about Object Aliasing
3:30 p.m., Wean Hall 8220
January 28, 2004
John C. Reynolds
Carnegie Mellon University and BRICS
TOWARDS A GRAINLESS SEMANTICS FOR SHARED VARIABLE CONCURRENCY
3:30 p.m., Wean Hall 8220
February 11, 2004
Benjamin C. Pierce
University of Pennsylvania
Harmony:  A Synchronization Framework for Tree-Structured Data
3:30 p.m., Wean Hall 8220
March 19, 2004
Jonathan Aldrich
Carnegie Mellon University
3:30 p.m., Wean Hall 8220
April 14, 2004
James Cheney
Cornell University
Logic Programming with Names and Binding
3:30 p.m., Wean Hall 8220
May 19, 2004 Patricia Johann
Rutgers University
Free Theorems in the Presence of seq
3:30 p.m., Wean Hall 8220
May 20, 2004
Peter Sewell
University of Cambridge
Distributed Interaction: Abstraction, Rebinding, and Version Control
3:30 p.m., Wean Hall 8220




Fall 2003


September 19, 2003 John Boyland
University of Wisconsin - Milwaukee
Checking interference with fractional permissions
3:30 p.m., Wean Hall 8220
September 26, 2003 Donna Malayeri
Carnegie Mellon University
Specifying and Checking Exception Effects in Fugue
3:30 p.m., Wean Hall 8220
October 22, 2003 Daniel Spoonhower
Carnegie Mellon University
Automatic Memory Management Using Regions for Object-Oriented Programs
3:30 p.m., Wean Hall 8220
December 3, 2003
Lujo Bauer
Carnegie Mellon University
Access Control on the Web via Proof-Carrying Authorization
3:30 p.m., Wean Hall 8220




Spring 2003


January 24, 2003 John C. Reynolds
Carnegie Mellon University
Separation Logic: A Logic for Shared Mutable Data Structures
3:30 p.m., Wean Hall 8220
February 7, 2003
K. Subramani
West Virginia University
An Analysis of Quantified Linear Programs
3:30 p.m., Wean Hall 8220
March 5, 2003 Tobias Nipkow
Technische Universität München
Proving Pointer Programs in Higher-Order Logic
3:30 p.m, NSH 1507
April 2, 2003
Josh Berdine
Carnegie Mellon University
Control Contexts versus Continuations in Linearly Typed CPS
3:30 p.m., Wean Hall 8220


Fall 2002

August 28, 2002
Geoff Washburn
University of Pennsylvania
Type Inference in System I and Extensions for Sums
3:30 p.m., Wean Hall 8220
October 2, 2002
Vivek Sarkar
IBM T. J. Watson Research Center
The Jikes Research Virtual Machine
3:30 p.m., Wean Hall 8220
October 9, 2002
Marcelo Fiore
University of Cambridge
Imaginary Types
1:30 p.m., Wean Hall 8220
December 4, 2002
Nuel Belnap
University of Pittsburgh
Is branching space-times theory useful in understanding parallel processing?
3:30 p.m., Wean Hall 8220
December 13, 2002
David Tarditi
Microsoft
Phoenix: an infrastructure for compilers and programming tools
3:30 p.m., Wean Hall 8220




Summer 2002

July 12, 2002 Andrew Bernard
Carnegie Mellon University
Temporal Logic for Proof-Carrying Code
3:30 p.m., Wean Hall 8220




Spring 2002
January 11, 2002
Umut A. Acar
Adaptive Functional Programming

3:30pm, Wean 8220
January 30, 2002
David S. Warren
State University of New York at Stony Brook 
Applications of a General Evaluation Strategy for Recursive Definitions

3:30pm, Wean 8220
February 8, 2002
Laurent Réveillère
Informatique et Radiocummunications de Bordeaux
Towards the Development of Robust Device Drivers

3:30pm, Wean 8220
March 1, 2002
Mircea Marin
University of Tsukuba
Collaborative Constraint Functional Logic Programming in Open Environments

3:30pm, Wean 8220
March 29, 2002
Peter O'Hearn
University of London
Separation Logic for Shared-Variable Concurrency

3:30pm, Wean 8220
April 26, 2002
Dirk Van Gucht 
Indiana University
Resource Bounded Computing in Databases

3:30pm, Wean 8220
May 10, 2002 Alberto Momigliano
Carnegie Mellon University
Combining Higher Order Abstract Syntax with Tactical Theorem Proving
and (Co)Induction
3:30 pm, Wean 8220




Fall 2001

October 26, 2001
Jakob Rehof
Microsoft Research
Types as Models: Model Checking Message-Passing Programs

3:30pm, Wean 8220
November 2, 2001
Eli Barzilay
Cornell University
Concrete Abstraction for End-User Computing in Creative Applications

3:30pm, Wean 8220
November 30, 2001
Jim Lipton
Weslyan University
Semantics of Higher Order Logic Programing

3:30pm, Wean 8220
December 7, 2001
Rob O'Callahan
IBM Research
Efficient and Precise Dynamic Race Detection for Object Oriented Programs

3:30pm, Wean 8220




Spring 2001
 
January 31, 2001 Gabi Keller
University of South Wales
Fast Functional Arrays
3:30pm, Wean 8220
February 1, 2001 Gabi Keller
University of South Wales
Fusion for Data Parallelism
12 noon, Wean 7220 -- **note: unusual date and time**
February 2, 2001 Iliano Cervesato
ITT Industries
MSR, a framework for specifying security protocols and investigating their meta-theory
3:30pm, Wean 8220
February 23, 2001 Cristiano Calcagno
Dipartimento di Informatica e Scienze dell'Informazione
Program logics in the presence of Garbage Collection
3:30pm, Wean 8220
March 7, 2001 Ursula Martin
University of St. Andrews
Computational math: the new challenge for computational logic
3:30pm, Wean 8220
April 6, 2001 Prakash Panangaden
McGill University
From Logic to Stochastic Processes
3:30pm, Wean 8220
April 25, 2001 Susan Eisenbach
Imperial College
Changing Java Programs
3:30pm, Wean 8220




Fall 2000
 
September 28, 2000 Peter Lee
Carnegie Mellon University
A Certifying Compiler for Java
12 noon, HH D-210
September 28, 2000 Henning Makholm
University of Copenhagen
Towards a More Flexible Region Type System
3:00pm, Wean 7220
September 29, 2000 Abbas Edalat
Imperial College
Domain Theory and Differential Calculus
3:30pm, Wean 8220
October 25, 2000 Robert Findler
Rice University
The Architecture of Dr Scheme or How to Build Extensible Software
3:30pm, Wean 8220
November 17, 2000 Heiko Mantel
Deduction and Multi-Agent System Lab
A Framework for Information Flow Control
2:00pm, Newell Simon 3002
December 15, 2000 Michael Hicks
Cornell University
Dynamic Software Updating
3:30pm, Wean 8220




Summer 2000
 
July 26, 2000 John C. Reynolds
Carnegie Mellon University
Intrinsic and Extrinsic Semantics of Intersection Types
3:30pm, Wean 8220




Spring 2000

April 7, 2000 Zhong Shao
Yale University
Fully Reflexive Intensional Type Analysis
3:30pm, Wean 8220
April 25, 2000 David Walker
Cornell University
Alias Types
3:00pm, Wean 4623
May 3, 2000 Peter O'Hearn
Queen Mary and Westfield College
BI as an Assertion Language for Mutable Data Structures
3:30pm, Wean 8220
May 12, 2000 Leaf Petersen
Carnegie Mellon University
Implementing the Internal Language of the TILT Compiler
3:30pm, Wean 8220
May 23, 2000 David Notkin
University of Washington
Symbolic Model Checking for Large Software Specifications: Case Studies, Optimization, and Extension
3:30pm, Wean 4623
May 26, 2000 Andreas Abel
Ludwig Maximilians University
Termination of Mutual Recursive Functions
3:30pm, Wean 8220




Fall 1999

August 12, 1990 James Harland
Royal Melbourne Institute of Technology
Computational Interpretations of Resource-Sensitive Logics
3:30pm, Wean 4623
August 20, 1999 Benjamin Pierce
University of Pennsylvania
What is a File Synchronizer?
3:30pm, Wean 8220
September 8, 1999 John Reynolds
Carnegie Mellon University
Reasoning about Shared Mutable Data Structure
3:30pm, Wean 8220
September 15, 1999 Craig Chambers
University of Washington
Modular, Statically Typed Multimethods in Dubious
3:30pm, Wean 8220




Spring 1999

January 27, 1999 Mads Tofte
DIKU
A Polymorphic Type Discipline for Solving Year 2000 Problems in COBOL
3:30pm, Wean 8220
February 3, 1999 Mark Lillibridge
Compaq SRC
Extended Static Checking for Java
3:30pm, Wean 8220
February 12, 1999 Nevin Heintze and Jon Riecke
Bell Labs
Security, Dependency and Regions
3:30pm, Wean 8220
April 21, 1999 Philip Wickline
Carnegie Mellon University
The PML Compiler: From Modal Logic to Run-Time Code Generation
3:30pm, Wean 8220
April 28, 1999 Aaron Greenhouse
Carnegie Mellon University
An Object-Oriented Effects System
3:30pm, Wean 8220
June 4, 1999 Michael Mendler
University of Sheffield
Lax Logic and its Application to the Timing Analysis of Combinational Systems
3:30pm, Wean 8220
June 9, 1999 John Boyland
University of Wisconsin-Madison
Alias Killing: Unique Variables Without Destructive Reads
3:30pm, Wean 8220




Fall 1998

September 18, 1998 Greg Nelson
Compaq SRC
3:30pm, Wean 8220
September 25, 1998 Leaf Petersen
Carnegie Mellon University
The Ambient Calculus
3:30pm, Wean 8220
October 7, 1998 Uday Reddy
University of Illinois
Objects and classes in Algol-like Languages
3:30pm, Wean 8220
October 30, 1998 Rob O'Callahan
Carnegie Mellon University
A Simple, Comprehensive Type System for Java Bytecode Subroutines
3:30pm, Wean 8220
November 6, 1998 Steve Zdancewic
Cornell University
A Syntactic Account of Type Abstraction
Noon, Wean 8220
November 18, 1998 Sebastian Thrun
Carnegie Mellon University
Towards a New Programming Language for Embedded Systems
3:30pm, Wean 8220
November 20, 1998 Mark Wegman
IBM T.J. Watson Research Center
Global Trends in Flow Analysis
Noon, Wean 4601
December 1, 1998 Gopalan Nadathur
University of Chicago
Issues in the Design and Implementation of a Higher-Order Metalanguage
1:30pm, Wean 4601
December 2, 1998 Dexter Kozen
Cornell University
Efficient Code Certification
3:30pm, Wean 8220
December 9, 1998 Kathleen Fisher
AT&T Research
Foundations for Moby Classes
3:30pm, Wean 8220


[Top]

Email the Maintainer
Modified: 12-February-2013