POP Seminar


Principles of Programming Seminar
Fall 2013
November, 25, 2013	Andrew Sogokon Research Postgraduate Student at the University of Edinburgh, United Kingdom Positive Invariance In Safety Verification Host: Andre Platzer 1:00 PM, Gates-Hillman Center- 6501
November 19, 2013	Limin Jia Assistant Research Professor at 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 University A Grainless Semantics for Parallel Programs with Shared Mutable Data 3:30 p.m., Wean Hall 5409
October 7, 2005	Jan Vitek Purdue University 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 University of Iowa DPLL-based Checkers for Satisfiability Modulo Theories 3:30 p.m., Wean Hall 4623
October 29, 2004	Simon Peyton Jones Microsoft Research Practical type inference for Generalised Algebraic Data Types 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 Compiling Relational Queries Over Program Traces To Instrumentation (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 Open Modules: A Proposal for Modular Reasoning in Aspect-Oriented Programming 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

Fall 2013

Spring 2013

Fall 2012

2011

2010

Fall 2009

Summer 2009

Spring 2009

Fall 2008

Summer 2008

Spring 2008

Fall 2007

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

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

Spring 2007

Fall 2006

Spring 2006

Fall 2005

Spring 2005

Summer 2005

Fall 2004

Summer 2004

Spring 2004

Fall 2003

Spring 2003

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

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