Robert J. Simmons: Home →
Research
A chronological list of papers sorted into the usual categories can be found below. A couple of recurring themes in my research come with project names, and for some others I've made a page summarizing the topic and linking to some relevant research:
- Constructive provability logic - a wild modal logic for reflecting on provability within proofs.
- L10 - declarative, distributed logic programming.
- Substructural logic programming - efficient and/or expressive extensions to forward-chaining logic programming.
- Meta-CLF - reasoning about the logical specification of distributed systems.
Dissertation: Substructural Logical Specifications
Available here or as a CMU tech report.
Recent
- A Logical Correspondence between Natural Semantics and Abstract Machines Robert J. Simmons and Ian Zerny. Short talk at LICS 2013. [PDF][ACM Free for full PPDP version]
- Structural focalization. Robert J. Simmons. TOCL, July 2014. [PDF] [arXiv] [ACM Free]
- Constructive Provability Logic. Robert J. Simmons and Bernardo Toninho. Submitted. [PDF] [arXiv]
Refereed Journal Publications
- Logical approximation for program analysis. Robert J. Simmons and Frank Pfenning. Higher Order and Symbolic Computation (special issue on Partial Evaluation and Program Manipulation 2009), 24(1-2):41-80. [PDF of accepted version] [Springer/HOSC] [Corrections]
- Products of Weighted Logic Programs. Shay B. Cohen, Robert J. Simmons, and Noah A. Smith. Theory and Practice of Logic Programming, 11(2-3):263-296. 2011. [PDF as published] [Cambridge/TPLP]
- Proofs from Tests. Nels E. Beckman, Aditya V. Nori, Sriram K. Rajamani, Robert J. Simmons, Sai Deep Tetali, and Aditya V. Thakur. IEEE Transactions on Software Engineering, 36(4):495-508. July/August 2010. [IEEE DL] [IEEE Xplore]
Refereed Conference Publications
- Substructural Operational Semantics as Ordered Logic Programming. Frank Pfenning and Robert J. Simmons. IEEE Symposium on Logic in Computer Science. August 2009. [IEEE Xplore]
- Linear logical approximations. Robert J. Simmons and Frank Pfenning. ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation. January 2009. [PDF author's version] [ACM DL] [ACM Free]
- Dynamic Programming Algorithms as Products of Weighted Logic Programs. Shay B. Cohen, Robert J. Simmons, and Noah A. Smith. International Conference on Logic Programming. In Logic Programming, LNCS 5366. December 2008. (Given the Best Student Paper Award.) [Springer] [Technical report (PDF)]
- Proofs from Tests. Nels Beckman, Aditya Nori, Sriram Rajamani, and Rob Simmons. ACM SIGSOFT International Symposium on Software Testing and Analysis. July 2008. [MSR Tech Report] [ACM DL] [ACM Free]
- Linear Logical Algorithms. Robert J. Simmons and Frank Pfenning. International Colloquium on Automata, Languages and Programming (Track B). In Automata, Languages and Programming, LNCS 5126. July 2008. [Springer] [CSD Tech Report]
Workshop Papers and Technical Reports
- Relating Reasoning Methodologies in Linear Logic and Process Algebra Yuxin Deng, Iliano Cervesato, and Robert J. Simmons. Accepted to LINEARITY 2012. [PDF]
- Relating Reasoning Methodologies in Linear Logic and Process Algebra Yuxin Deng, Robert J. Simmons, and Iliano Cervesato Technical report CMU-CS-11-145, Carnegie Mellon University, Department of Computer Science. December 2011. [PDF] [CMU Tech Report Link]
- Constructive Provability Logic. Robert J. Simmons and Bernardo Toninho. Intuitionistic Modal Logic and Applications Workshop. July 2011. [PDF] [Agda code @ Bitbucket]
- Distributed deductive databases, declaratively: The L10 logic programming language. Robert J. Simmons, Frank Pfenning, and Bernardo Toninho. X10 Workshop. June 2011. [PDF]
- Weak Focusing for Ordered Linear Logic. Robert J. Simmons and Frank Pfenning. Technical report CMU-CS-10-147, Carnegie Mellon University, Department of Computer Science. April 2011. [PDF] [CMU Tech Report Link]
- Principles of Constructive Provability Logic. Robert J. Simmons and Bernardo Toninho. Technical report CMU-CS-10-151, Carnegie Mellon University, Department of Computer Science. December 2010. [PDF] [CMU Tech Report Link]
- Type Safety for Substructural Specifications: Preliminary Results. Robert J. Simmons. Technical report CMU-CS-10-134, Carnegie Mellon University, Department of Computer Science. July 2010. [PDF] [CMU Tech Report Link] (A corrected and slightly condensed version of my thesis proposal.)
- SASyLF: An Educational Proof Assistant for Language Theory. Jonathan Aldrich, Robert J. Simmons, and Key Shin. ACM SIGPLAN Workshop on Functional and Declarative Programming Education. September 2008. [ICFP Poster (PDF)] [ACM DL] [ACM Free]
- Mechanized Metatheory for User-Defined Type Extensions. Daniel Marino, Brian Chin, Todd Millstein, Gang Tan, Robert J. Simmons, and David Walker. ACM SIGPLAN Workshop on Mechanizing Metatheory. September 2006. [PDF]
- Twelf as a unified framework for language formalization and implementation. Robert J. Simmons. Princeton University undergraduate senior thesis 18679. [PDF] [Associated Code]
Slides and miscellaneous notes
- Cut admissibility for focused multiplicative, exponential linear logic. Note (partially scanned off of paper). [PDF]
- Constructive Provability Logic. After-the-fact slide recording of talk presented at the Workshop on Intuitionistic Modal Logic and Applications. July 2011. [YouTube]
- Logic Programming in Constructive Provability Logic. Robert J. Simmons and Bernardo Toninho. Course project for Modal Logic. May 2010. [PDF]
- Attacking and defending PCM-based main memory Milo Polte and Robert J. Simmons. Course project for Advanced Computer Architecture, Spring 2009. [PDF slides]
-
The Proof Theory of the Logic of Bunched Implications.
Slides from two talks given at the Current Research on Separation Logic seminar at Carnegie Mellon.
April 2009.
Part 1, The Logic of Bunched Implications: [PDF]
Part 2, Display Logics for Classical and Boolean Bunched Implications: [PDF] - Logical specification and coinduction. Half-baked note, rejected with cause at ICLP 2009. November 2008. [PDF]
- Linear Logical Algorithms. After-the-fact slide recording of talk presented at the International Conference on Automata, Languages, and Programming. July 2008. [Quicktime]
- Concurrent Algorithms in Linear Logic Programming. At the informal "New Programming Models and Tools for Concurrency" workshop, Carnegie Mellon University. February 2008. [PDF]
- Netezza meets MapReduce: Abstractions for data intensive computing. Severin Hacker, Robert J. Simmons, and Carsten Varming. Course project for Advanced and Distributed Operating Systems. Fall 2007. [PDF] [PDF slides]
-
LF and Twelf.
Two lectures given at Microsoft Research, India.
August 2007.
Part 1, The LF Logical Framework. [PDF] [Flash]
Part 2, The Twelf Metalogical Framework. [PDF] [Flash] - The LF Seminar: Term Representation. My writeup of a lecture given by Frank Pfenning. February 2007. [PDF] Aleksey Kliger, Ruy Ley-Wild, and course Frank Pfenning provided corrections and feedback.
- Metatheoretic approaches to programming language specification and verification. At the Princeton TACL Seminar. April 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. After RFL #7 I discontinued the series and moved future thoughts to the Request for Logic blog.
- RFL #7 - Higher order focusing for ordered logic (3/4/10, with Dan Licata and Jason Reed)
- RFL #6 - Linear functions and coverage checking stuff with holes in it (12/14/09)
- RFL #5 - The inverse method and backward chaining in ordered logic (12/6/09)
- RFL #4 - Embedding Logics in Other Logics (12/3/09)
- RFL #3 - Encoding Substructural Logics in a Hybrid Framework (11/22/09)
- RFL #2 - What Would A Polarized Logical Framework Be Good For? (10/9/09)
- RFL #1 - Mismatch II (10/2/09)