I am a lecturer (equivalent to an assistant professor) at the Computer Laboratory, at the University of Cambridge.
Before that, I was a Birmingham Fellow at the University of Birmingham, in the Theory Group. Before that, I was 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.
Neel Krishnaswami
University of Cambridge
Computer Laboratory
William Gates Building
15 JJ Thomson Avenue
Cambridge CB3 0FD, UK
Sound and Complete Bidirectional Typechecking for Higher-Rank Polymorphism and Indexed Types, Joshua Dunfield and Neelakantan R. Krishnaswami. Submitted July 2018.
A technical report with complete proofs is also available.
→ Abstract
Bidirectional typechecking, in which terms either synthesize a type or are checked against a known type, has become popular for its scalability, its error reporting, and its ease of implementation. Following principles from proof theory, bidirectional typing can be applied to many type constructs. The principles underlying a bidirectional approach to indexed types (generalized algebraic datatypes) are less clear. Building on proof-theoretic treatments of equality, we give a declarative specification of typing based on focalization. This approach permits declarative rules for coverage of pattern matching, as well as support for first-class existential types using a focalized subtyping judgment. We use refinement types to avoid explicitly passing equality proofs in our term syntax, making our calculus close to languages such as Haskell and OCaml. An explicit rule deduces when a type is principal, leading to reliable substitution principles for a rich type system with significant type inference.
We also give a set of algorithmic typing rules, and prove that it is sound and complete with respect to the declarative system. The proof requires a number of technical innovations, including proving soundness and completeness in a mutually-recursive fashion.
A Typed, Algebraic Approach to Parsing, Neelakantan R. Krishnaswami and Jeremy Yallop. Draft, submitted for publication July 2018.
→ Abstract
In this paper, we recall the definition of the context-free expressions (or μ-regular expressions), an algebraic presentation of the context-free languages. Then, we define a core type system for the context-free expressions to pick out those expressions which can be parsed unambiguously by predictive algorithms such as recursive descent or LL(k) style tabular parsing. Next, we extend the notion of Brzozowski derivative from regular expressions to the typed context-free expressions. Finally, we define a type system for context-free expressions which permits left-recursive and non-left-factored expressions, and which elaborates them into equivalent into core terms. All of these type systems and algorithms are proved sound with respect to the denotational semantics of context-free expressions.
ISA Semantics for ARMv8-A, RISC-V, and CHERI-MIPS, Alasdair Armstrong, Thomas Bauereiss, Brian Campbell, Alastair Reid, Kathryn E. Gray, Robert M. Norton, Prashanth Mundkur, Mark Wassell, Jon French, Christopher Pulte, Shaked Flur, Ian Stark, Neel Krishnaswami, Peter Sewell. Draft, submitted for publication July 2018.
→ Abstract
Architecture specifications notionally define the fundamental interface between hardware and software: the envelope of allowed behaviour for processor implementations, and the basic assumptions for software development and verification. But in practice, they are typically prose and pseudocode documents, not rigorous or executable artifacts, leaving software and verification on shaky ground.
In this paper, we present rigorous semantic models for the sequential behaviour of large parts of the mainstream ARMv8-A, RISC-V, and MIPS architectures, and the research CHERI-MIPS architecture, that are complete enough to boot operating systems, variously Linux, FreeBSD, or seL4. Our ARMv8-A models are automatically translated from authoritative ARM-internal definitions, and (in one variant) tested against the ARM Architecture Validation Suite.
We do this using a custom language for ISA semantics, Sail, with a lightweight dependent type system, that supports automatic generation of emulator code in C and OCaml, and automatic generation of proof-assistant definitions for Isabelle, HOL4, and (currently only for MIPS) Coq. We use the former for validation, and to assess specification coverage. To demonstrate the usability of the latter, we prove (in Isabelle) correctness of a purely functional characterisation of ARMv8-A address translation. We moreover integrate the RISC-V model into the RMEM tool for (user-mode) relaxed-memory concurrency exploration. We prove (on paper) the soundness of the core Sail type system.
We thereby take a big step towards making the architectural abstraction actually well-defined, establishing foundations for verification and reasoning.
The Essence of Event-Driven Programming, Jennifer Paykin, Neelakantan R. Krishnaswami, and Steve Zdancewic. Draft.
→ Abstract
Event-driven programming is based on a natural abstraction: an event is a computation that can eventually return a value. This paper exploits the intuition relating events and time by drawing a Curry-Howard correspondence between a functional event-driven programming language and a linear-time temporal logic. In this logic, the eventually proposition ◇A describes the type of events, and Girard’s linear logic describes the effectful and concurrent nature of the programs. The correspondence reveals many interesting insights into the nature of event- driven programming, including a generalization of selective choice for synchronizing events, and an implementation in terms of callbacks where ◇A is just ¬□¬A.
Datafun: a Functional Datalog, Michael Arntzenius and Neelakantan R. Krishnaswami. Accepted for publication at ICFP 2016.
→ Abstract → BibTeX
Datalog may be considered either an unusually powerful query language or a carefully limited logic programming language. It has been applied successfully in a wide variety of problem domains thanks to its "sweet spot" combination of expressivity, optimizability, and declarativeness. However, most use-cases require extending Datalog in an application-specific manner. In this paper we define Datafun, an analogue of Datalog supporting higher-order functional programming. The key idea is to track monotonicity via types.
@inproceedings{datafun, author = {Arntzenius, Michael and Krishnaswami, Neelakantan R.}, title = {Datafun: A Functional Datalog}, booktitle = {Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming}, series = {ICFP 2016}, year = {2016}, isbn = {978-1-4503-4219-3}, location = {Nara, Japan}, pages = {214--227}, numpages = {14}, url = {http://doi.acm.org/10.1145/2951913.2951948}, doi = {10.1145/2951913.2951948}, acmid = {2951948}, publisher = {ACM}, address = {New York, NY, USA}, keywords = {Datalog, Prolog, adjoint logic, denotational semantics, domain-specific languages, functional programming, logic programming, operational semantics, type theory}, }
Mtac: A Monad for Typed Tactic Programming in Coq, Beta Ziliani, Derek Dreyer, Neelakantan R. Krishnaswami, Aleksandar Nanevski, Viktor Vafeiadis. To appear in the Journal of Functional Programming.
A website with Coq source and tutorial is available.
→ Abstract → BibTeX
Effective support for custom proof automation is essential for large-scale interactive proof development. However, existing languages for automation via tactics either (a) provide no way to specify the behavior of tactics within the base logic of the accompanying 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 that supports 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 these new tactical primitives in a monad, and instrumenting Coq so that it executes monadic tactics during type inference.@article{mtac-journal, title = "Mtac: A monad for typed tactic programming in Coq", doi = "10.1017/S0956796815000118", publisher = "Cambridge University Press", address = "Cambridge, UK", author = "Beta Ziliani and Derek Dreyer and Neelakantan R. Krishnaswami and Aleksandar Nanevski and Viktor Vafeiadis", volume = "25", year = "2015", month = "001", day = "001", url = "https://www.cambridge.org/core/article/mtac-a-monad-for-typed-tactic-programming-in-coq/75B49F20037D8A0F718EAB21C662ABA0", journal = "Journal of Functional Programming" }
Integrating Linear and Dependent Types, Neelakantan R. Krishnaswami, Pierre Pradic, Nick Benton. Accepted for publication at POPL 2015. The technical report with proofs is also available.
→ Abstract → BibTeX
In this paper, we show how to integrate linear types with type dependency, by extending the linear/non-linear calculus of Benton to support type dependency.
Next, we give an application of this calculus by giving a proof-theoretic account of imperative programming, which requires extending the calculus with computationally irrelevant quantification, proof irrelevance, and a monad of computations. We show the soundness of our theory by giving a realizability model in the style of Nuprl, which permits us to validate not only the β-laws for each type, but also the η-laws.
These extensions permit us to decompose Hoare triples into a collection of simpler type-theoretic connectives, yielding a rich equational theory for dependently-typed higher-order imperative programs. Furthermore, both the type theory and its model are relatively simple, even when all of the extensions are considered.
@InProceedings{dlnl15, author = {Neelakantan R. Krishnaswami and Pierre Pradic and Nick Benton}, title = {Integrating Linear and Dependent Types}, booktitle = {Principles of Programming Languages (POPL)}, month = jan, year = {2015}, note = {\url{http://www.cs.bham.ac.uk/~krishnan/dlnl-paper.pdf}} }
Freeze After Writing: Quasi-Deterministic Parallel Programming with LVars and Handlers, Lindsey Kuper, Aaron Turon, Neelakantan R. Krishnaswami, Ryan Newton. Accepted for publication at POPL 2014.
→ Abstract → BibTeX
Deterministic-by-construction parallel programming models offer programmers the promise of freedom from subtle, hard-to-reproduce nondeterministic bugs in parallel code. A principled approach to deterministic-by-construction parallel programming with shared state is offered by LVars: shared memory locations whose semantics are defined in terms of a user-specified lattice. Writes to an LVar take the least upper bound of the old and new values with respect to the lattice, while reads from an LVar can observe only that its contents have crossed a specified threshold in the lattice. Although it guarantees determinism, this interface is quite limited.
We extend LVars in two ways. First, we add the ability to "freeze" and then read the contents of an LVar directly. Second, we add the ability to attach callback functions to an LVar, allowing events to be triggered by writes to it. Together, callbacks and freezing enable an expressive and useful style of parallel programming. We prove that in a language where communication takes place through freezable LVars, programs are at worst quasi-deterministic: on every run, they either produce the same answer or raise an error. We demonstrate the viability of our approach by implementing a library for Haskell supporting a variety of LVar-based data structures, together with two case studies that illustrate the programming model and yield promising parallel speedup.
@InProceedings{kuper14lvish, author = {Lindsey Kuper and Aaron Turon and Neelakantan R. Krishnaswami and Ryan Newton}, title = {Freeze After Writing: Quasi-Deterministic Parallel Programming with LVars and Handlers}, booktitle = {Principles of Programming Languages (POPL)}, month = jan, year = {2014}, note = {\url{http://www.cs.indiana.edu/~lkuper/papers/lvish-popl14.pdf}} }
Complete and Easy Bidirectional Typechecking for Higher-Rank Polymorphism, Joshua Dunfield and Neelakantan R. Krishnaswami. Accepted for publication at ICFP 2013. A companion tech report with detailed proofs is also available.
Joshua Dunfield has his own web page for the paper, too.
→ Abstract → BibTeX
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.
@InProceedings{Dunfield13:bidir, author = {Joshua Dunfield and Neelakantan R. Krishnaswami}, title = {Complete and Easy Bidirectional Typechecking for Higher-Rank Polymorphism}, booktitle = {International Conference on Functional Programming (ICFP)}, month = sep, year = {2013}, note = {\url{arXiv:1306.6032 [cs.PL]}} }
Higher-Order Reactive Programming without Spacetime Leaks, Neelakantan R. Krishnaswami. Accepted for publication at ICFP 2013. The companion tech report with the soundness proof is also available.
Download the source for the AdjS programming language implementing the theory!
→ Abstract → BibTeX
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.
@InProceedings{Krishnaswami13:simple-frp, author = {Neelakantan R. Krishnaswami}, title = {Higher-Order Reactive Programming without Spacetime Leaks}, booktitle = {International Conference on Functional Programming (ICFP)}, month = sep, year = {2013}, }
Mtac: A Monad for Typed Tactic Programming in Coq , Beta Ziliani, Derek Dreyer, Neelakantan R. Krishnaswami, Aleksandar Nanevski, Viktor Vafeiadis. Accepted for publication at ICFP 2013.
See the Mtac homepage for more details, including software!
→ Abstract → BibTeX
Effective support for custom proof automation is essential for large-scale interactive proof development. However, existing languages for automation via 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.
@InProceedings{Ziliani13:mtac, author = {Beta Ziliani, Derek Dreyer, Neelakantan R. Krishnaswami, Aleksandar Nanevski, Viktor Vafeiadis}, title = {Mtac: A Monad for Typed Tactic Programming in Coq}, booktitle = {International Conference on Functional Programming (ICFP)}, month = sep, year = {2013}, }
Internalizing Relational Parametricity in the Extensional Calculus of Constructions, Neelakantan R. Krishnaswami, Derek Dreyer. Accepted for publication at CSL 2013. The tech report with expanded proofs is also be available.
→ Abstract → BibTeX
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.@InProceedings{KrishnaswamiDreyer13:relpar, author = {Neelakantan R. Krishnaswami, Derek Dreyer}, title = {Internalizing Relational Parametricity in the Extensional Calculus of Constructions}, booktitle = {Computer Science Logic (CSL)}, month = sep, year = {2013}, }
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
Curry-Howard for GUIs: Or, User Interfaces via Linear Temporal, Classical Linear Logic, Jennifer Paykin, Neel Krishnaswami, Steve Zdancewic. Unpublished draft.
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.