I am a postdoc at the Max Planck Institute for Software Systems, working with Derek Dreyer.
Before that, I was a postdoc at Microsoft Research, working with Nick Benton, and before that, I was a Ph.D. student under the supervision of John C. Reynolds and Jonathan Aldrich.
This coming fall, I will join the Theory Group at the University of Birmingham.
Complete and Easy Bidirectional Typechecking for Higher-Rank Polymorphism, Joshua Dunfield and Neelakantan R. Krishnaswami. Submitted. A companion tech report with detailed proofs is also available.
Joshua Dunfield has his own web page for the paper, too.
→ Abstract
Bidirectional typechecking, in which terms either synthesize a type or are checked against a known type, has become popular for its scalability (unlike Damas-Milner type inference, bidirectional typing remains decidable even for very expressive type systems), its error reporting, and its relative ease of implementation. Following design principles from proof theory, bidirectional typing can be applied to many type constructs. The principles underlying a bidirectional approach to polymorphism, however, are less obvious. We give a declarative, bidirectional account of higher-rank polymorphism, grounded in proof theory; this calculus enjoys many properties such as η-reduction and predictability of annotations. We give an algorithm for implementing the declarative system; our algorithm is remarkably simple and well-behaved, despite being both sound and complete.
Higher-Order Reactive Programming without Spacetime Leaks, Neelakantan R. Krishnaswami. Submitted. The companion tech report with the soundness proof is also available.
Download the source for the AdjS programming language implementing the theory!
→ Abstract
Functional reactive programming (FRP) is an elegant approach to declaratively specify reactive systems. However, the powerful abstractions of FRP have historically made it difficult to predict and control the resource usage of programs written in this style.
In this paper, we give a new language for higher-order reactive programming. This language generalizes and simplifies prior type systems for reactive programming, supporting the use of first-class streams, such as streams of streams; first-class functions and higher-order operations; and permits encoding many temporal operations beyond streams, such as terminatable streams, events, and even resumptions with first-class schedulers. Furthermore, our language supports an efficient implementation strategy permitting us to eagerly deallocate old values and statically rule out spacetime leaks, a notorious source of inefficiency in reactive programs. Furthermore, these memory guarantees are achieved without the use of a complex substructural type discipline.
We also show that our implementation strategy of eager deallocation is safe, by showing the soundness of our type system with a novel step-indexed Kripke logical relation.
Mtac: A Monad for Typed Tactic Programming in Coq , Beta Ziliani, Derek Dreyer, Neelakantan R. Krishnaswami, Aleksandar Nanevski, Viktor Vafeiadis.
See the Mtac homepage for more details, including software!
→ Abstract
Effective support for custom proof automation is essential for large-scale interactive proof development. However, existing languages for automation via \emph{tactics} either (a) provide no way to specify the behavior of tactics statically within the logic of the theorem prover or (b) rely on advanced type-theoretic machinery that is not easily integrated into established theorem provers.
We present Mtac, a lightweight but powerful extension to Coq for supporting dependently-typed tactic programming. Mtac tactics have access to all the features of ordinary Coq programming, as well as a new set of typed tactical primitives. We avoid the need to touch the trusted kernel typechecker of Coq by encapsulating uses of the new tactical primitives in a monad, and instrumenting Coq so that it executes monadic tactics during type inference.
Internalizing Relational Parametricity in the Extensional Calculus of Constructions, Neelakantan R. Krishnaswami, Derek Dreyer. Under submission. The tech report with expanded proofs is also be available.
→ Abstract
We give the first relationally parametric model of the extensional calculus of constructions. Our model remains as simple as traditional PER models of types, but unlike them, it additionally permits the relating of terms that implement abstract types in different ways. Using our model, we can validate the soundness of quotient types, as well as derive strong equality axioms for Church-encoded data, such as the usual induction principles for Church naturals and booleans, and the eta law for strong dependent pair types. Furthermore, we show that such equivalences, justified by relationally parametric reasoning, may soundly be internalized (i.e. added as equality axioms to our type theory). Thus, we demonstrate that it is possible to interpret equality in a dependently-typed setting using parametricity. The key idea behind our approach is to interpret types as so-called quasi-PERs (or zigzag-complete relations), which enable us to model the symmetry and transitivity of equality while at the same time allowing for different representations of abstract types.Conference Papers
Superficially Substructural Types, Neelakantan R. Krishnaswami, Aaron Turon, Derek Dreyer, Deepak Garg. Accepted for publication at ICFP 2012. The extended tech report is also available.
→ Abstract → BibTeX
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 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 work 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.
@inproceedings{krishnaswami-turon-dreyer-garg:superficial, title = {Superficially Substructural Types}, author = {Neelakantan R. Krishnaswami and Aaron Turon and Derek Dreyer and Deepak Garg}, booktitle = {Proceedings of the 17th annual ACM SIGPLAN-SIGACT International Conference on Functional Programming}, series = {ICFP '12}, year = {2012}, month = {September}, day = {10-12}, location = {Copenhagen, Denmark}, publisher = {ACM}, address = {New York, NY, USA}, keywords = {linear logic, aliasing, separation logic, sharing, step-indexing, logical relations}, }Adding Equations to System F Types, Neelakantan R. Krishnaswami, Nick Benton. Appeared 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
Verifying Higher-Order Imperative Programs with Higher-Order Separation LogicHistory
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.
Neelakantan R. Krishnaswami <neelk@mpi-sws.org> Last modified: Fri Mar 29 16:29:05 CET 2013