Conference Papers and Journal Articles
Provably Correct, Asymptotically Efficient, HigherOrder ReverseMode Automatic Differentiation, Faustyna Krawiec, Simon PeytonJones, Neel Krishnaswami, Tom Ellis, Richard A. Eisenberg, and Andrew Fitzgibbon. Accepted for publication at POPL 2022.
In this paper, we give a simple and efficient implementation of reversemode automatic differentiation, which both extends easily to higherorder functions, and has run time and memory consumption linear in the run time of the original program. In addition to a formal description of the translation, we also describe an implementation of this algorithm, and prove its correctness by means of a logical relations argument.
@article{higherorderad, author = {Faustyna Krawiec and Simon PeytonJones and Neel Krishnaswami and Tom Ellis and Richard A. Eisenberg and Andrew Fitzgibbon }, title = {Provably Correct, Asymptotically Efficient, HigherOrder ReverseMode Automatic Differentiation}, journal = {{PACMPL}}, volume = {6}, number = {{POPL}}, year = {2022}, note = {\url{http://www.cl.cam.ac.uk/~nk480/higherorderad.pdf}} }Adjoint Reactive GUI Programming, Christial Uldal Graulund, Dimitrij Szamozvancev, and Neel Krishnaswami. Draft, submitted for publication. Link to ArXiV version
Most interaction with a computer is done via a graphical user interface. Traditionally, these are implemented in an imperative fashion using shared mutable state and callbacks. This is efficient, but is also difficult to reason about and error prone. Functional Reactive Programming (FRP) provides an elegant alternative which allows GUIs to be designed in a declarative fashion. However, most FRP languages are synchronous and continually check for new data. This means that an FRPstyle GUI will "wake up" on each program cycle. This is problematic for applications like text editors and browsers, where often nothing happens for extended periods of time, and we want the implementation to sleep until new data arrives. In this paper, we present an asynchronous FRP language for designing GUIs called λ𝖶𝗂𝖽𝗀𝖾𝗍. Our language provides a novel semantics for widgets, the building block of GUIs, which offers both a natural CurryHoward logical interpretation and an efficient implementation strategy.
@InProceedings{10.1007/9783030719951_15, author="Graulund, Christian Uldal and Szamozvancev, Dmitrij and Krishnaswami, Neel", editor="Kiefer, Stefan and Tasson, Christine", title="Adjoint Reactive GUI Programming", booktitle="Foundations of Software Science and Computation Structures", year="2021", publisher="Springer International Publishing", address="Cham", pages="289309", isbn="9783030719951" }Bidirectional Typechecking, Jana Dunfield and Neel Krishnaswami. To appear in ACM Computing Surveys. Link to ArXiV version
Bidirectional typing combines two modes of typing: type checking, which checks that a program satisfies a known type, and type synthesis, which determines a type from the program. Using checking enables bidirectional typing to break the decidability barrier of DamasMilner approaches; using synthesis enables bidirectional typing to avoid the large annotation burden of explicitly typed languages. In addition, bidirectional typing improves error locality. We highlight the design principles that underlie bidirectional type systems, survey the development of bidirectional typing from the prehistoric period before Pierce and Turner's local type inference to the present day, and provide guidance for future investigations.
@Unpublished{Dunfield21:bidirsurvey, author = {Jana Dunfield and Neel Krishnaswami}, title = {Bidirectional Typing}, year = {2021}, note = {\url{arXiv:1908.05839 [cs.PL]}} }Transfinite StepIndexing for Termination, Simon Spies, Neel Krishnaswami and Derek Dreyer. Accepted for publication at POPL 2021.
(See also the MPI website, and also the PDF with full proofs.)
Stepindexed logical relations are an extremely useful technique for building operationalsemanticsbased models and program logics for realistic, richlytyped programming languages. They have proven to be indispensable for modeling features like higherorder state, which many languages support but which were difficult to accommodate using traditional denotational models. However, the conventional wisdom is that, because they only support reasoning about finite traces of computation, (unary) stepindexed models are only good for proving safety properties like “welltyped programs don’t go wrong”. There has consequently been very little work on using stepindexing to establish liveness properties, in particular termination.
In this paper, we show that stepindexing can in fact be used to prove termination of welltyped programs  even in the presence of dynamicallyallocated, shared, mutable, higherorder state—so long as one’s type system enforces disciplined use of such state. Specifically, we consider a language with asynchronous channels, inspired by promises in JavaScript, in which higherorder state is used to implement communication, and linearity is used to ensure termination. The key to our approach is to generalize from natural number stepindexing to transfinite stepindexing, which enables us to compute termination bounds for program expressions in a compositional way. Although transfinite stepindexing has been proposed previously, we are the first to apply this technique to reasoning about termination in the presence of higherorder state.
@article{seminaivedatafun, author = {Simon Spies and Neel Krishnaswami and Derek Dreyer}, title = {Transfinite StepIndexing for Termination}, journal = {{PACMPL}}, volume = {5}, number = {{POPL}}, pages = {13:11:328}, year = {2021} note = {\url{http://www.cl.cam.ac.uk/~nk480/transfinitestepindexing.pdf}} }Recovering Purity with Comonads and Capabilities, Vikraman Chaudhury and Neel Krishnaswami. Accepted for publication at ICFP 2020.
See also the technical report with complete proofs.
In this paper, we take a pervasively effectful (in the style of ML) typed lambda calculus, and show how to extend it to permit capturing pure expressions with types. Our key observation is that, just as the pure simply typed lambda calculus can be extended to support effects with a monadic type discipline, an impure typed lambda calculus can be extended to support purity with a comonadic type discipline.
We establish the correctness of our type system via a simple denotational model, which we call the capability space model. Our model formalizes the intuition common to systems programmers that the ability to perform effects should be controlled via access to a permission or capability, and that a program is capability safe if it performs no effects that it does not have a runtime capability for. We then identify the axiomatic categorical structure that the capability space model validates, and use these axioms to give a categorical semantics for our comonadic type system. We then give an equational theory (substitution and the callbyvalue β and η laws) for the imperative lambda calculus, and show its soundness relative to this semantics.
Finally, we give a translation of the pure simplytyped lambda calculus into our comonadic imperative calculus, and show that any two terms which are βηequal in the STLC are equal in the equational theory of the comonadic calculus, establishing that pure programs can be mapped in an equationpreserving way into our imperative calculus.
@article{comonadiccapabilities, author = {Vikraman Chaudhury and Neel Krishnaswami }, title = {Recovering Purity with Comonads and Capabilities}, journal = {{PACMPL}}, volume = {4}, number = {{POPL}}, pages = {111:1111:328}, year = {2021} note = {\url{http://www.cl.cam.ac.uk/~nk480/icfp20cap.pdf}} }Seminaïve Evaluation for a HigherOrder Functional Language, Michael Arntzenius and Neel Krishnaswami. Accepted for publication at POPL 2020. Won Distinguished Paper Award.
One of the workhorse techniques for implementing bottomup Datalog engines is seminaïve evaluation. This optimization improves the performance of Datalog’s most distinctive feature: recursively defined predicates. These are computed iteratively, and under a naïve evaluation strategy, each iteration recomputes all previous values. Seminaïve evaluation computes a safe approximation of the difference between iterations. This can asymptotically improve the performance of Datalog queries.
Seminaïve evaluation is defined partly as a program transformation and partly as a modified iteration strategy, and takes advantage of the firstorder nature of Datalog code. This paper extends the seminaïve transformation to higherorder programs written in the Datafun language, which extends Datalog with features like firstclass relations, higherorder functions, and datatypes like sum types.
@article{seminaivedatafun, author = {Michael Arntzenius and Neel Krishnaswami}, title = {Seminaïve Evaluation for a HigherOrder Functional Language}, journal = {{PACMPL}}, volume = {3}, number = {{POPL}}, pages = {9:19:28}, year = {2020} note = {\url{http://www.cl.cam.ac.uk/~nk480/seminaivedatafun.pdf}} }A Typed, Algebraic Approach to Parsing, Neel Krishnaswami and Jeremy Yallop. Draft, accepted for publication at PLDI 2019. Won Distinguished Paper Award.
In this paper, we recall the definition of the contextfree expressions (or µregular expressions), an algebraic presentation of the contextfree languages. Then, we define a core type system for the contextfree expressions which gives a compositional criterion for identifying those contextfree expressions which can be parsed unambiguously by predictive algorithms in the style of recursive descent or LL(1).
Next, we show how these typed grammar expressions can be used to derive a parser combinator library which both guarantees lineartime parsing with no backtracking and singletoken lookahead, and which respects the natural denotational semantics of contextfree expressions. Finally, we show how to exploit the type information to write a staged version of this library, which produces dramatic increases in performance, even outperforming code generated by the standard parser generator tool ocamlyacc.
@InProceedings{parsingpldi19, author = {Neel Krishnaswami and Jeremy Yallop}, title = {A Typed, Algebraic Approach to Parsing}, booktitle = {Programming Language Design and Implementation (PLDI)}, month = jun, year = {2019}, note = {\url{http://www.cl.cam.ac.uk/~nk480/parsing.pdf}} }NumLin: Linear Types for Linear Algebra, Dhruv Makwana and Neel Krishnaswmi. Draft, accepted for publication at ECOOP 2019.
We present NumLin, a functional programming language designed to express the APIs of lowlevel linear algebra libraries (such as BLAS/LAPACK) safely and explicitly, through a brief description of its key features and several illustrative examples. We show that NumLin’s type system is sound and that its implementation improves upon naïve implementations of linear algebra programs, almost towards Clevels of performance. Lastly, we contrast it to other recent developments in linear types and show that using linear types and fractional permissions to express the APIs of lowlevel linear algebra libraries is a simple and effective idea.
@InProceedings{numlinecoop19, author = {Dhruv Makwana and Neel Krishnaswami}, title = {NumLin: Linear Types for Linear Algebra}, booktitle = {European Conference On Programming languages (ECOOP)}, month = jul, year = {2019}, note = {\url{http://www.cl.cam.ac.uk/~nk480/numlin.pdf}} }A Program Logic for FirstOrder Encapsulated WebAssembly, Conrad Watt, Petar Maksimov, Neel Krishnaswami, Phillipa Gardner. Draft, accepted for publication at ECOOP 2019.
We introduce Wasm Logic, a sound program logic for firstorder, encapsulated WebAssembly.
We design a novel assertion syntax, tailored to WebAssembly's stackbased semantics and the strong guarantees given by WebAssembly's type system, and show how to adapt the standard separation logic triple and proof rules in a principled way to capture WebAssembly's uncommon structured control flow. Using Wasm Logic, we specify and verify a simple WebAssembly Btree library, giving abstract specifications independent of the underlying implementation.
We mechanise Wasm Logic and its soundness proof in full in Isabelle/HOL. As part of the soundness proof, we formalise and fully mechanise a novel, bigstep semantics of WebAssembly, which we prove equivalent, up to transitive closure, to the original WebAssembly smallstep semantics.
@InProceedings{wasmecoop19, author = {Conrad Watt and Petar Maksimov and Neel Krishnaswami and Phillipa Gardner}, title = {A Program Logic for FirstOrder Encapsulated WebAssembly}, booktitle = {European Conference On Programming languages (ECOOP)}, month = jul, year = {2019}, note = {\url{http://www.cl.cam.ac.uk/~nk480/wasmpl.pdf}} }ISA Semantics for ARMv8A, RISCV, and CHERIMIPS, 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. Accepted for publication at POPL 2019.
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 ARMv8A, RISCV, and MIPS architectures, and the research CHERIMIPS architecture, that are complete enough to boot operating systems, variously Linux, FreeBSD, or seL4. Our ARMv8A models are automatically translated from authoritative ARMinternal 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 proofassistant 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 ARMv8A address translation. We moreover integrate the RISCV model into the RMEM tool for (usermode) relaxedmemory 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 welldefined, establishing foundations for verification and reasoning.
@inproceedings{sailpopl2019, author = {Alasdair Armstrong and Thomas Bauereiss and Brian Campbell and Alastair Reid and Kathryn E. Gray and Robert M. Norton and Prashanth Mundkur and Mark Wassell and Jon French and Christopher Pulte and Shaked Flur and Ian Stark and Neel Krishnaswami and Peter Sewell}, title = {{ISA} Semantics for {ARMv8A, RISCV, and CHERIMIPS}}, optcrossref = {}, optkey = {}, conf = {POPL 2019}, booktitle = {\textbf{POPL 2019}: Proc. 46th ACM SIGPLAN Symposium on Principles of Programming Languages}, optbooktitle = {}, year = {2019}, opteditor = {}, optvolume = {}, optnumber = {}, optseries = {}, optpages = {}, month = jan, optaddress = {}, optorganization = {}, optpublisher = {}, note = {Proc. ACM Program. Lang. 3, POPL, Article 71}, optnote = {}, optannote = {}, doi = {10.1145/3290384}Sound and Complete Bidirectional Typechecking for HigherRank Polymorphism and Indexed Types, Jana Dunfield and Neelakantan R. Krishnaswami. Accepted for publication at POPL 2019.
A technical report with complete proofs is also available.
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 prooftheoretic 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 firstclass 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 mutuallyrecursive fashion.
@InProceedings{gadtpopl19, author = {Jana Dunfield and Neel Krishnaswami}, title = {Sound and Complete Bidirectional Typechecking for HigherRank Polymorphism and Indexed Types}, booktitle = {Principles of Programming Languages (POPL)}, month = jan, year = {2019}, note = {\url{http://www.cl.cam.ac.uk/~nk480/gadt.pdf}} }Datafun: a Functional Datalog, Michael Arntzenius and Neelakantan R. Krishnaswami. Accepted for publication at ICFP 2016.
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 usecases require extending Datalog in an applicationspecific manner. In this paper we define Datafun, an analogue of Datalog supporting higherorder 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 = {9781450342193}, location = {Nara, Japan}, pages = {214227}, numpages = {14}, url = {https://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, domainspecific 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.
Effective support for custom proof automation is essential for largescale 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 typetheoretic machinery that is not easily integrated into established theorem provers.
We present Mtac, a lightweight but powerful extension to Coq that supports dependentlytyped 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{mtacjournal, 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/mtacamonadfortypedtacticprogrammingincoq/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.
In this paper, we show how to integrate linear types with type dependency, by extending the linear/nonlinear calculus of Benton to support type dependency.
Next, we give an application of this calculus by giving a prooftheoretic 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 typetheoretic connectives, yielding a rich equational theory for dependentlytyped higherorder 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/dlnlpaper.pdf}} }Freeze After Writing: QuasiDeterministic Parallel Programming with LVars and Handlers, Lindsey Kuper, Aaron Turon, Neelakantan R. Krishnaswami, Ryan Newton. Accepted for publication at POPL 2014.
Deterministicbyconstruction parallel programming models offer programmers the promise of freedom from subtle, hardtoreproduce nondeterministic bugs in parallel code. A principled approach to deterministicbyconstruction parallel programming with shared state is offered by LVars: shared memory locations whose semantics are defined in terms of a userspecified 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 quasideterministic: 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 LVarbased 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: QuasiDeterministic Parallel Programming with LVars and Handlers}, booktitle = {Principles of Programming Languages (POPL)}, month = jan, year = {2014}, note = {\url{https://www.cs.indiana.edu/~lkuper/papers/lvishpopl14.pdf}} }Complete and Easy Bidirectional Typechecking for HigherRank Polymorphism, Jana Dunfield and Neelakantan R. Krishnaswami. Accepted for publication at ICFP 2013. A companion tech report with detailed proofs is also available.
Jana Dunfield has a web page for the paper, too.
Bidirectional typechecking, in which terms either synthesize a type or are checked against a known type, has become popular for its scalability (unlike DamasMilner 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 higherrank 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 wellbehaved, despite being both sound and complete.
@InProceedings{Dunfield13:bidir, author = {Jana Dunfield and Neelakantan R. Krishnaswami}, title = {Complete and Easy Bidirectional Typechecking for HigherRank Polymorphism}, booktitle = {International Conference on Functional Programming (ICFP)}, month = sep, year = {2013}, note = {\url{arXiv:1306.6032 [cs.PL]}} }HigherOrder 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!
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 higherorder reactive programming. This language generalizes and simplifies prior type systems for reactive programming, supporting the use of firstclass streams, such as streams of streams; firstclass functions and higherorder operations; and permits encoding many temporal operations beyond streams, such as terminatable streams, events, and even resumptions with firstclass 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 stepindexed Kripke logical relation.
@InProceedings{Krishnaswami13:simplefrp, author = {Neelakantan R. Krishnaswami}, title = {HigherOrder 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!
Effective support for custom proof automation is essential for largescale 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 typetheoretic machinery that is not easily integrated into established theorem provers.
We present Mtac, a lightweight but powerful extension to Coq for supporting dependentlytyped 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.
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 Churchencoded 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 dependentlytyped setting using parametricity. The key idea behind our approach is to interpret types as socalled quasiPERs (or zigzagcomplete 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.
Many substructural type systems have been proposed for controlling access to shared state in higherorder 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 coarsegrained 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 finegrained 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 resourceoriented Kripke logical relation.
@inproceedings{krishnaswamiturondreyergarg: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 SIGPLANSIGACT International Conference on Functional Programming}, series = {ICFP '12}, year = {2012}, month = {September}, day = {1012}, location = {Copenhagen, Denmark}, publisher = {ACM}, address = {New York, NY, USA}, keywords = {linear logic, aliasing, separation logic, sharing, stepindexing, logical relations}, }Adding Equations to System F Types, Neelakantan R. Krishnaswami, Nick Benton. Appeared at ESOP 2012.
We present an extension of System F with types for termlevel 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{krishnaswamibenton: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 = {SpringerVerlag} }HigherOrder Functional Reactive Programming in Bounded Space, Neelakantan R. Krishnaswami, Nick Benton, Jan Hoffmann. Accepted for publication at POPL 2012.
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 discretetime 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 higherorder functions and highertype 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 wellfounded.
We also give a denotational semantics for our language by combining recent work on metric spaces for the interpretation of higherorder causal functions with lengthspace models of spacebounded computation. The resulting category is doubly closed and hence forms a model of the logic of bunched implications.
@inproceedings{krishnaswamibentonhoffmann:hofrp, author = {Krishnaswami, Neelakantan R. and Benton, Nick and Hoffmann, Jan}, title = {Higherorder functional reactive programming in bounded space}, booktitle = {Proceedings of the 39th annual ACM SIGPLANSIGACT symposium on Principles of programming languages}, series = {POPL '12}, year = {2012}, isbn = {9781450310833}, location = {Philadelphia, PA, USA}, pages = {4558}, numpages = {14}, url = {https://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, spacebounded computation}, }A Semantic Model for Graphical User Interfaces, Neelakantan R. Krishnaswami, Nick Benton. Appeared in ICFP 2011.
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 wellfounded 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/nonlinear domainspecific language for writing GUI programs. The nonlinear part of the language is used for writing reactive streamprocessing 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{krishnaswamibenton:guisemantics, 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 = {9781450308656}, location = {Tokyo, Japan}, pages = {4557}, numpages = {13}, url = {https://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.
We describe a denotational model of higherorder 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 lowlevel implementation is correct with respect to the highlevel semantics.
@inproceedings{krishnaswamibenton:ultrametricfrp, 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 = {9780769544120}, pages = {257266}, numpages = {10}, url = {https://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.
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 CurryHoward 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:patternmatching, author = {Krishnaswami, Neelakantan R.}, title = {Focusing on pattern matching}, booktitle = {Proceedings of the 36th annual ACM SIGPLANSIGACT symposium on Principles of programming languages}, series = {POPL '09}, year = {2009}, isbn = {9781605583792}, location = {Savannah, GA, USA}, pages = {366378}, numpages = {13}, url = {https://doi.acm.org/10.1145/1480881.1480927}, doi = {10.1145/1480881.1480927}, acmid = {1480927}, publisher = {ACM}, address = {New York, NY, USA}, keywords = {curryhoward, focusing, pattern matching, type theory}, }PermissionBased Ownership: Encapsulating State in HigherOrder Typed Languages, Neel Krishnaswami and Jonathan Aldrich. Appeared in PLDI 2005.
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 adhoc access restrictions and are limited to Javalike 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 = {Permissionbased ownership: encapsulating state in higherorder typed languages}, booktitle = {Proceedings of the 2005 ACM SIGPLAN conference on Programming language design and implementation}, series = {PLDI '05}, year = {2005}, isbn = {1595930566}, location = {Chicago, IL, USA}, pages = {96106}, numpages = {11}, url = {https://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 SpringerVerlag)
The inverse method, due to Maslov, is a forward theorem proving method for cutfree 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{donnellygibsonkrishnaswamimagillpark: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 = {466480}, url = {https://dx.doi.org/10.1007/9783540322757_31}, series = {Lecture Notes in Computer Science}, volume = {3452}, location = {Montevideo, Uraguay}, publisher = {SpringerVerlag}, keywords = {bunched implications, inverse method, theorem proving} }
Workshop Papers
Representing Music with Prefix Trees, Yan Han, Nada Amin, Neel Krishnaswami. FARM 2019.
Tonal music contains repeating or varying patterns that occur at various scales, exist at multiple locations, and embody diverse properties of musical notes. We define a language for representing music that expresses such patterns as musical transformations applied to multiple locations in a score. To concisely represent collections of patterns with shared struc ture, we organize them into prefix trees. We demonstrate the effectiveness of this approach by using it to recreate a complete piece of tonal music.
@inproceedings{krishnaswamibirkedalaldrich:ramifiedframes, author = {Han, Yan and Amin, Nada and Krishnaswami, Neel}, title = {Representing Music with Prefix Trees}, booktitle = {The ACM SIGPLAN International Workshop on Functional Art, Music, Modelling and Design (FARM)}, series = {FARM '19}, year = {2019}, location = {Berlin, Germany}, numpages = {12}, publisher = {ACM}, address = {New York, NY, USA}, keywords = {prefix tree, music representation, Haskell}, }Verifying EventDriven Programs using Ramified Frame Properties, Neelakantan R. Krishnaswami, Jonathan Aldrich, Lars Birkedal. Appeared in TLDI 2010.
Interactive programs, such as GUIs or spreadsheets, often maintain dependency information over dynamicallycreated 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 dynamicallygenerated 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 applicationspecific 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{krishnaswamibirkedalaldrich:ramifiedframes, author = {Krishnaswami, Neel R. and Birkedal, Lars and Aldrich, Jonathan}, title = {Verifying eventdriven 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 = {9781605588919}, location = {Madrid, Spain}, pages = {6376}, numpages = {14}, url = {https://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, subjectobserver}, }Design Patterns in Separation Logic, Neelakantan R. Krishnaswami, Jonathan Aldrich, Lars Birkedal, Kasper Svendsen, Alexandre Buisse. Appeared in TLDI 2009.
Objectoriented programs are notable for making use of both higherorder 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{krishnaswamialdrichbirkedalsvendsenbuisse:designpatterns, 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 = {9781605584201}, location = {Savannah, GA, USA}, pages = {105116}, numpages = {12}, url = {https://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}, }
Thesis

Verifying HigherOrder Imperative Programs with HigherOrder Separation Logic, Neel Krishnaswami. 2011.
In this thesis I show is that it is possible to give modular correctness proofs of interesting higherorder imperative programs using higherorder separation logic.
To do this, I develop a model higherorder imperative programming language, and develop a program logic for it. I demonstrate the power of my program logic by verifying a series of examples. This includes both realistic patterns of higherorder imperative programming such as the subjectobserver pattern, as well as examples demonstrating the use of higherorder logic to reason modularly about highly aliased data structures such as the unionfind disjoint set algorithm.
@phdthesis{phdthesis, author = {Neelakantan R. Krishnaswami}, title = {Verifying HigherOrder Imperative Programs with HigherOrder Separation Logic}, school = {Carnegie Mellon University}, year = 2011, address = {Pittsburgh, PA, USA.}, month = 7 }
Working Drafts
Implicit Polarized F: Local Type Inference for Impredicativity, Henry Mercer, Cameron Ramsay, and Neel Krishnaswami. Draft.
System F, the polymorphic lambda calculus, features the principle of impredicativity: polymorphic types may be explicitly instantiated at other types, enabling many powerful idioms such as Church encoding and data abstraction. Unfortunately, type applications need to be implicit for a language to be humanusable, and the problem of inferring all type applications in System F is undecidable. As a result, language designers have historically avoided impredicative type inference.
We reformulate System F in terms of callbypushvalue, and study type inference for it. Surprisingly, this new perspective yields a novel type inference algorithm which is extremely simple to implement (not even requiring unification), infers many types, and has a simple declarative specification. Furthermore, our approach offers type theoretic explanations of how many of the heuristics used in existing algorithms for impredicative polymorphism arise.
Fusing Lexing and Parsing, Jeremy Yallop, Ningning Xie, and Krishnaswami. Draft.
Lexers and parsers are typically defined separately and connected by a token stream. This separate definition is important for modularity, but harmful for performance.
We show how to fuse together separatelydefined lexers and parsers, drastically improving performance without compromising modularity. Our staged parser combinator library, flap, provides a standard parser combinator interface, but generates specialized tokenfree code that runs several times faster than ocamlyacc on a range of benchmarks.
Older Drafts
Mechanised Metatheory for the Sail ISA Specification Language, Mark Wassell, Alasdair Armstrong, Neel Krishnaswami, Peter Sewell. Draft.
Sail is a language for rigorous specification of instruction set architectures (ISAs); it has been used to model various production and research architectures, including ARMv8A, RISCV, and CHERIMIPS, sufficiently completely to boot multiple operating systems. Intended to be engineer friendly, Sail is an imperative firstorder language with a lightweight dependent type system; it can generate OCaml and C emulators and Isabelle, HOL4, and Coq definitions. A recent substantial redesign of the Sail type system has been done in conjunction with the development of a core calculus, Mini Sail, along with paper proofs of type safety.
This paper presents further work to mechanise MiniSail in the Isabelle theorem prover, making use of the Nominal2 Isabelle library to address binding structures and alphaequivalence; it includes the definition of the MiniSail type system and operational semantics and proofs of preservation and progress. We discuss how the mechanisation and paper formalisations relate to each other, including the benefits and pitfalls of each, and comment on how these have influenced and been influenced by the Sail implementation redesign. We also comment on whether the use of Nominal Isabelle allows us to write proofs of programming language safety that are human readable as well as being machine verified. This mechanisation should in future provide a platform for the mechanical generation of a verified implementation of a type checker and evaluator for the language.
The Essence of EventDriven Programming, Jennifer Paykin, Neelakantan R. Krishnaswami, and Steve Zdancewic. Draft.
Eventdriven 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 CurryHoward correspondence between a functional eventdriven programming language and a lineartime 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.
CurryHoward for GUIs: Or, User Interfaces via Linear Temporal, Classical Linear Logic, Jennifer Paykin, Neel Krishnaswami, Steve Zdancewic. Unpublished draft.
Modular Verification of the SubjectObserver Pattern via HigherOrder Separation Logic, Neelakantan R. Krishnaswami, Lars Birkedal, and Jonathan Aldrich. Unpublished draft, presented at the FTFJP 2007 workshop.
Separation Logic for a HigherOrder 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 cutelimination, 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.
Students
PhD Students
 Michael Arntzenius (20152021)
 Dima Szamozvancev (2018) (with Marcelo Fiore)
 Andrej Ivašković (2018) (with Alan Mycroft)
 Faustyna Krawiec (2020)
 Dhruv Makwana (2019)
 Angus Hammond (2020)
 Ilia Kaisin (2021)
 Jad Ghalayini (2021)
Master's Students
 Rosie Baish (20202021)
 Wojiech Nawrocki (20192020)
 Cameron Ramsay (20192020)
 Simon P. Spies (20192020)
 Henry Mercer (201819)
 Yan Han (201819)
 Dhruv Makwana (201718)
 Dima Szamozvancev (201718)
 Jan Christian Menz (201617)
Personal History
Before coming to Cambridge, 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.
Actual History
Gordon Plotkin, Lambdadefinability 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.