Neelakantan R. Krishnaswami

Work

Latest Research

Superficially Substructural Types, Neelakantan R. Krishnaswami, Aaron Turon, Derek Dreyer, Deepak Garg. Under submission. The extended tech report is also available.

→ Abstract

Many substructural type systems have been proposed for controlling access to shared state in higher-order languages. Central to these systems is the notion of a resource, which may be split into disjoint pieces that different parts of a program can manipulate independently without worrying about interfering with one another. Some systems support a logical notion of resource (such as permissions), under which two resources may be considered disjoint even if they govern the \emph{same} piece of state. However, in nearly all existing systems, the notions of resource and disjointness are fixed at the outset, baked into the model of the language, and fairly coarse-grained in the kinds of sharing they enable.

In this paper, inspired by recent wokr on "fictional disjointness" in separation logic, we propose a simple and flexible way of enabling any module in a program to create its own custom type of splittable resource (represented as a commutative monoid), thus providing fine-grained control over how the module's private state is shared with its clients. This functionality can be incorporated into an otherwise standard substructural type system by means of a new typing rule we call the sharing rule, whose soundness we prove semantically via a novel resource-oriented Kripke logical relation.

Conference Papers

• Adding Equations to System F Types, Neelakantan R. Krishnaswami, Nick Benton. Accepted for publication at ESOP 2012.

  → Abstract → BibTeX

  We present an extension of System F with types for term-level equations. This internalization of the rich equational theory of the polymorphic lambda calculus yields an expressive core language, suitable for formalizing features such as Haskell's rewriting rules mechanism or Extended ML signatures.

  	      @inproceedings{krishnaswami-benton:feqn,
  	        title = {Adding Equations to System F Types},
  	        author = {Neelakantan R. Krishnaswami and Nick Benton},
  	        year  = {2012},
  	        month = {March},
  	        day   = {26},
  	        location = {Tallinn, Estonia},
  	        booktitle = {21st European Symposium on Programming (ESOP 2012)},
  	        series = {Lecture Notes in Computer Science},
  	        publisher = {Springer-Verlag}
  	      }
  	    

• Higher-Order Functional Reactive Programming in Bounded Space, Neelakantan R. Krishnaswami, Nick Benton, Jan Hoffmann. Accepted for publication at POPL 2012.

  → Abstract → BibTeX

  Functional reactive programming (FRP) is an elegant and successful approach to programming reactive systems declaratively. The high levels of abstraction and expressivity that make FRP attractive as a programming model do, however, often lead to programs whose resource usage is excessive and hard to predict.

  In this paper, we address the problem of space leaks in discrete-time functional reactive programs. We present a functional reactive programming language that statically bounds the size of the dataflow graph a reactive program creates, while still permitting use of higher-order functions and higher-type streams such as streams of streams. We achieve this with a novel linear type theory that both controls allocation and ensures that all recursive definitions are well-founded.

  We also give a denotational semantics for our language by combining recent work on metric spaces for the interpretation of higher-order causal functions with length-space models of space-bounded computation. The resulting category is doubly closed and hence forms a model of the logic of bunched implications.

  	      @inproceedings{krishnaswami-benton-hoffmann:ho-frp,
  	       	author = {Krishnaswami, Neelakantan R. and Benton, Nick and Hoffmann, Jan},
  	       	title = {Higher-order functional reactive programming in bounded space},
  	       	booktitle = {Proceedings of the 39th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages},
  	       	series = {POPL '12},
  	       	year = {2012},
  	       	isbn = {978-1-4503-1083-3},
  	       	location = {Philadelphia, PA, USA},
  	       	pages = {45--58},
  	       	numpages = {14},
  	       	url = {http://doi.acm.org/10.1145/2103656.2103665},
  	       	doi = {10.1145/2103656.2103665},
  	       	acmid = {2103665},
  	       	publisher = {ACM},
  	       	address = {New York, NY, USA},
  	       	keywords = {bunched implications, dataflow, functional reactive programming, linear logic, space-bounded computation},
  	      } 
  	    

• A Semantic Model for Graphical User Interfaces, Neelakantan R. Krishnaswami, Nick Benton. Appeared in ICFP 2011.

  → Abstract → BibTeX

  We give a denotational model for graphical user interface (GUI) programming using the Cartesian closed category of ultrametric spaces. The ultrametric structure enforces causality restrictions on reactive systems and allows well-founded recursive definitions by a generalization of guardedness. We capture the arbitrariness of user input (e.g., a user gets to \emph{decide} the stream of clicks she sends to a program) by making use of the fact that the closed subsets of an ultrametric space themselves form an ultrametric space, allowing us to interpret nondeterminism with a ``powerspace'' monad.

  Algebras for the powerspace monad yield a model of intuitionistic linear logic, which we exploit in the definition of a mixed linear/non-linear domain-specific language for writing GUI programs. The non-linear part of the language is used for writing reactive stream-processing functions whilst the linear sublanguage naturally captures the generativity and usage constraints on the various linear objects in GUIs, such as the elements of a DOM or scene graph.

  We have implemented this DSL as an extension to OCaml, and give examples demonstrating that programs in this style can be short and readable.

  	      @inproceedings{krishnaswami-benton:gui-semantics,
  	       	author = {Krishnaswami, Neelakantan R. and Benton, Nick},
  	       	title = {A semantic model for graphical user interfaces},
  	       	booktitle = {Proceedings of the 16th ACM SIGPLAN international conference on Functional programming},
  	       	series = {ICFP '11},
  	       	year = {2011},
  	       	isbn = {978-1-4503-0865-6},
  	       	location = {Tokyo, Japan},
  	       	pages = {45--57},
  	       	numpages = {13},
  	       	url = {http://doi.acm.org/10.1145/2034773.2034782},
  	       	doi = {10.1145/2034773.2034782},
  	       	acmid = {2034782},
  	       	publisher = {ACM},
  	       	address = {New York, NY, USA},
  	       	keywords = {denotational semantics, functional reactive programming, guarded recursion, linear logic, ultrametric spaces},
  	      } 
  	    

• Ultrametric Semantics of Reactive Programs, Neelakantan R. Krishnaswami, Nick Benton. Preprint. Appeared in LICS 2011.

  You can download the source code for the implementation of the language in the paper. You need Ocaml 3.11 or higher, and the Lablgtk2 GUI library.

  → Abstract → BibTeX

  We describe a denotational model of higher-order functional reactive programming using ultrametric spaces and nonexpansive maps, which provide a natural Cartesian closed generalization of causal stream functions and guarded recursive definitions. We define a type theory corresponding to this semantics and show that it satisfies normalization. Finally, we show how to efficiently implement reactive programs written in this language using an imperatively updated dataflow graph, and give a separation logic proof that this low-level implementation is correct with respect to the high-level semantics.

  	      @inproceedings{krishnaswami-benton:ultrametric-frp,
  	       	author = {Krishnaswami, Neelakantan R. and Benton, Nick},
  	       	title = {Ultrametric Semantics of Reactive Programs},
  	       	booktitle = {Proceedings of the 2011 IEEE 26th Annual Symposium on Logic in Computer Science},
  	       	series = {LICS '11},
  	       	year = {2011},
  	       	isbn = {978-0-7695-4412-0},
  	       	pages = {257--266},
  	       	numpages = {10},
  	       	url = {http://dx.doi.org/10.1109/LICS.2011.38},
  	       	doi = {10.1109/LICS.2011.38},
  	       	acmid = {2059621},
  	       	publisher = {IEEE Computer Society},
  	       	address = {Washington, DC, USA},
  	      } 
  	    

• Focusing on Pattern Matching, Neelakantan R. Krishnaswami. Appeared in POPL 2009.

  → Abstract → BibTeX

  In this paper, we show how pattern matching can be seen to arise from a proof term assignment for the focused sequent calculus. This use of the Curry-Howard correspondence allows us to give a novel coverage checking algorithm, and makes it possible to give a rigorous correctness proof for the classical pattern compilation strategy of building decision trees via matrices of patterns.

  	      @inproceedings{krishnaswami:pattern-matching,
  	       	author = {Krishnaswami, Neelakantan R.},
  	       	title = {Focusing on pattern matching},
  	       	booktitle = {Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages},
  	       	series = {POPL '09},
  	       	year = {2009},
  	       	isbn = {978-1-60558-379-2},
  	       	location = {Savannah, GA, USA},
  	       	pages = {366--378},
  	       	numpages = {13},
  	       	url = {http://doi.acm.org/10.1145/1480881.1480927},
  	       	doi = {10.1145/1480881.1480927},
  	       	acmid = {1480927},
  	       	publisher = {ACM},
  	       	address = {New York, NY, USA},
  	       	keywords = {curry-howard, focusing, pattern matching, type theory},
  	      } 
  	    

• Permission-Based Ownership: Encapsulating State in Higher-Order Typed Languages, Neel Krishnaswami and Jonathan Aldrich. Appeared in PLDI 2005.

  → Abstract → BibTeX

  Today's module systems do not effectively support information hiding in the presence of shared mutable objects, causing serious problems in the development and evolution of large software systems. Ownership types have been proposed as a solution to this problem, but current systems have ad-hoc access restrictions and are limited to Java-like languages. In this paper, we describe System Fown, an extension of System F with references and ownership. Our design shows both how ownership fits into standard type theory and the encapsulation benefits it can provide in languages with firstclass functions, abstract data types, and parametric polymorphism. By looking at ownership in the setting of System F, we were able to develop a design that is more principled and flexible than previous ownership type systems, while also providing stronger encapsulation guarantees.

  	      @inproceedings{Krishnaswami:2005:POE:1065010.1065023,
  	       	author = {Krishnaswami, Neel and Aldrich, Jonathan},
  	       	title = {Permission-based ownership: encapsulating state in higher-order typed languages},
  	       	booktitle = {Proceedings of the 2005 ACM SIGPLAN conference on Programming language design and implementation},
  	       	series = {PLDI '05},
  	       	year = {2005},
  	       	isbn = {1-59593-056-6},
  	       	location = {Chicago, IL, USA},
  	       	pages = {96--106},
  	       	numpages = {11},
  	       	url = {http://doi.acm.org/10.1145/1065010.1065023},
  	       	doi = {10.1145/1065010.1065023},
  	       	acmid = {1065023},
  	       	publisher = {ACM},
  	       	address = {New York, NY, USA},
  	       	keywords = {domains, lambda calculus, modularity, ownership types, permissions, state, system f, type theory},
  	      } 
  	    

• The Inverse Method for the Logic of Bunched Implications, Kevin Donnelly, Tyler Gibson, Neel Krishnaswami, Steven Magill and Sungwoo Park. Appeared in LPAR 2004. (Copyright Springer-Verlag)

  → Abstract → BibTeX

  The inverse method, due to Maslov, is a forward theorem proving method for cut-free sequent calculi that relies on the subformula property. The Logic of Bunched Implications (BI), due to Pym and O'Hearn, is a logic which freely combines the familiar connectives of intuitionistic logic with multiplicative linear conjunction and its adjoint implication. We present the first formulation of an inverse method for propositional BI without units. We adapt the sequent calculus for BI into a forward calculus. The soundness and completeness of the calculus are proved, and a canonical form for bunches is given.

  	      @inproceedings{donnelly-gibson-krishnaswami-magill-park:bi,
  	        author    = {Kevin Donnelly and
  	                     Tyler Gibson and
  	                     Neel Krishnaswami and
  	                     Stephen Magill and
  	                     Sungwoo Park},
  	        title     = {The Inverse Method for the Logic of Bunched Implications},
  	        booktitle = {Logic for Programming, Artificial Intelligence, and Reasoning,
  	                     11th International Conference, LPAR 2004},
  	        year      = {2004},
  	        pages     = {466-480},
  	        url       = {http://dx.doi.org/10.1007/978-3-540-32275-7_31},
  	        series    = {Lecture Notes in Computer Science},
  	        volume    = {3452},
  	        location  = {Montevideo, Uraguay},
  	        publisher = {Springer-Verlag},
  	        keywords  = {bunched implications, inverse method, theorem proving}
  	      }
  	    

Published Workshop Papers

• Verifying Event-Driven Programs using Ramified Frame Properties, Neelakantan R. Krishnaswami, Jonathan Aldrich, Lars Birkedal. Appeared in TLDI 2010.

  → Abstract → BibTeX

  Interactive programs, such as GUIs or spreadsheets, often maintain dependency information over dynamically-created networks of objects. That is, each imperative object tracks not only the objects its own invariant depends on, but also all of the objects which depend upon it, in order to notify them when it changes.

  These bidirectional linkages pose a serious challenge to verification, because their correctness relies upon a global invariant over the object graph.

  We show how to modularly verify programs written using dynamically-generated bidirectional dependency information. The critical idea is to distinguish between the footprint of a command, and the state whose invariants depends upon the footprint. To do so, we define an application-specific semantics of updates, and introduce the concept of a ramification operator to explain how local changes can alter our knowledge of the rest of the heap. We illustrate the applicability of this style of proof with a case study from functional reactive programming, and formally justify reasoning about an extremely imperative implementation as if it were pure.

  	      @inproceedings{krishnaswami-birkedal-aldrich:ramified-frames,
  	       	author = {Krishnaswami, Neel R. and Birkedal, Lars and Aldrich, Jonathan},
  	       	title = {Verifying event-driven programs using ramified frame properties},
  	       	booktitle = {Proceedings of the 5th ACM SIGPLAN workshop on Types in language design and implementation},
  	       	series = {TLDI '10},
  	       	year = {2010},
  	       	isbn = {978-1-60558-891-9},
  	       	location = {Madrid, Spain},
  	       	pages = {63--76},
  	       	numpages = {14},
  	       	url = {http://doi.acm.org/10.1145/1708016.1708025},
  	       	doi = {10.1145/1708016.1708025},
  	       	acmid = {1708025},
  	       	publisher = {ACM},
  	       	address = {New York, NY, USA},
  	       	keywords = {dataflow, frame rule, functional reactive programming, ramification problem, separation logic, subject-observer},
  	      } 
  	    

• Design Patterns in Separation Logic, Neelakantan R. Krishnaswami, Jonathan Aldrich, Lars Birkedal, Kasper Svendsen, Alexandre Buisse. Appeared in TLDI 2009.

  → Abstract → BibTeX

  Object-oriented programs are notable for making use of both higher-order abstractions and mutable, aliased state. Either feature alone is challenging for formal verification, and the combination yields very flexible program designs and correspondingly difficult verification problems. In this paper, we show how to formally specify and verify programs that use several common design patterns in concert.

  	      @inproceedings{krishnaswami-aldrich-birkedal-svendsen-buisse:design-patterns,
  	       	author = {Krishnaswami, Neelakantan R. and Aldrich, Jonathan and Birkedal, Lars and Svendsen, Kasper and Buisse, Alexandre},
  	       	title = {Design patterns in separation logic},
  	       	booktitle = {Proceedings of the 4th international workshop on Types in language design and implementation},
  	       	series = {TLDI '09},
  	       	year = {2009},
  	       	isbn = {978-1-60558-420-1},
  	       	location = {Savannah, GA, USA},
  	       	pages = {105--116},
  	       	numpages = {12},
  	       	url = {http://doi.acm.org/10.1145/1481861.1481874},
  	       	doi = {10.1145/1481861.1481874},
  	       	acmid = {1481874},
  	       	publisher = {ACM},
  	       	address = {New York, NY, USA},
  	       	keywords = {design patterns, separation logic},
  	      } 
  	    

Some Drafts

• Modular Verification of the Subject-Observer Pattern via Higher-Order Separation Logic, Neelakantan R. Krishnaswami, Lars Birkedal, and Jonathan Aldrich. Unpublished draft, presented at the FTFJP 2007 workshop.

• Separation Logic for a Higher-Order Typed Language, Neel Krishnaswami. Unpublished draft, presented at SPACE 2006 workshop.

• A Modal Sequent Calculus for Propositional Separation Logic, Neelakantan R. Krishnaswami. Unpublished draft, presented at IMLA 2008 workshop (Intuitionistic Modal Logic and Applications). Note: the sequent calculus in this paper, while satisfying cut-elimination, is NOT sound with respect to the Kripke semantics of separation logic! The proof in the draft is incorrect.

• Idealized ML and Its Separation Logic, Neelakantan R. Krishnaswami, Lars Birkedal, Jonathan Aldrich, John C. Reynolds. Submitted for publication to POPL 2007.

Thesis

History

• Gordon Plotkin, Lambda-definability and Logical Relations, unpublished manuscript, Edinburgh 1973.

  This is where, as far as I know, the phrase "logical relation" originates.

  Update: Rick Statman tells me that Mike Gordon coined the phrase logical relation, and that he and Gordon Plotkin picked it up from him.