Papers, talks, and notes

Robert J. Simmons

Papers

[2009]

Substructural Operational Semantics as Ordered Logic Programming

With Frank Pfenning. Accepted to LICS 2009, August 11-14, 2009. [PDF][Related material]

Linear Logical Approximations

With Frank Pfenning. Presented at PEPM 2009, January 19-20, 2009. [PDF][ACM link]

[2008]

Dynamic Programming Algorithms as Products of Weighted Logic Programs

With Shay B. Cohen and Noah A. Smith. Presented at ICLP 2008, December 9-13 2008. Given the Best Student Paper Award. [SpringerLink] [LTI Tech Report]

SASyLF: An Educational Proof Assistant for Language Theory

With Jonathan Aldrich and Key Shin. Presented at FDPE 2008, September 21, 2008. [ICFP Poster (PDF)] [ACM link]

Proofs From Tests

With Nels Beckman, Aditya Nori, and Sriram K. Rajamini. Presented at ISSTA 2008, July 20, 2008. [ACM link] [MSR Tech Report]

Linear Logical Algorithms

With Frank Pfenning. Presented at ICALP 2008, July 6-13, 2008. [more]

[1982-2007]

Mechanized Metatheory for User-Defined Type Extensions

With Daniel Marino, Brian Chin, Todd Millstein, Gang Tan, and David Walker. Presented at the ACM SIGPLAN Workshop on Mechanizing Metatheory, September 21, 2006. [PDF][BibTeX]

Twelf as a unified framework for language formalization and implementation

Advised by David Walker. Princeton University undergraduate senior thesis 18679, April 29, 2005. [PDF] [Associated code][BibTeX]

Talks

The Logic of Bunched Implications (part 1 of 2)

At Carnegie Mellon's Current Research on Separation Logic course (15-818A4), April 6, 2009. [PDF]

Display Logics for Classical and Boolean Bunched Implications (part 2 of 2)

At Carnegie Mellon's Current Research on Separation Logic course (15-818A4), April 8, 2009. [PDF]

Concurrent Algorithms in Linear Logic Programming

At the informal "New Programming Models and Tools for Concurrency" workshop, Carnegie Mellon, February 14, 2008. A slightly different perspective on the material in "Linear Logical Algorithms." [PDF]

The LF Logical Framework (part 1 of 2)

At Microsoft Research, India, August 3, 2007. [PDF, Flash of Keynote talk]

The Twelf Metalogical Framework (part 2 of 2)

At Microsoft Research, India, August 13, 2007. [PDF, Flash of Keynote talk]
More information can be found on the Twelf Wiki

Metatheoretic approaches to programming language specification and verification

At the Princeton TACL Seminar, April 27, 2005. [Annotated Powerpoint slides]

RFL: Request for Logic

In 2009, partially inspired by Guglielmi's Mismatch and partially just frustrated with LaTeX, I started writing a bunch of Unicode fixed-width notes in Emacs, formatting them lightly in Word, and uploading them blog-style.

Notes

Attacking and defending PCM-based main memory

With Milo Polte. Course project for Advanced Computer Architecture, Spring 2009. [PDF slides]

Logical specification and coinduction

Fall 2008. [PDF]

Netezza meets MapReduce: Abstractions for data intensive computing

With Severin Hacker and Carsten Varming. Course project for Advanced and Distributed Operating Systems, Fall 2007. [PDF][PDF slides]

LF Group Meetings

I am attempting to keep a set of notes from Frank Pfenning's lectures from the LF group meetings which began in Spring of 2007. They can be found here.