4 citations · 6 across the 3 of their papers we have counts for
6 papers · 1 filter
Explicit Refinement Types
Jad Elkhaleq Ghalayini, Neel Krishnaswami
We present λert, a type theory supporting refinement types with explicit proofs. Instead of solving refinement constraints with an SMT solver like DML and Liquid Haskell, our syste…
Implicit Polarized F: local type inference for impredicativity
Henry Mercer, Cameron Ramsay, Neel Krishnaswami
System F, the polymorphic lambda calculus, features the principle of impredicativity: polymorphic types may be (explicitly) instantiated at other types, enabling many powerful idio…
Adjoint Reactive GUI
Christian Uldal Graulund, Dmitrij Szamozvancev, Neel Krishnaswami
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. Thi…
Recovering Purity with Comonads and Capabilities
Vikraman Choudhury, Neel Krishnaswami
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 observ…
A Program Logic for First-Order Encapsulated WebAssembly
Conrad Watt, Petar Maksimović, Neelakantan R. Krishnaswami +1
We introduce Wasm Logic, a sound program logic for first-order, encapsulated WebAssembly. We design a novel assertion syntax, tailored to WebAssembly's stack-based semantics and th…
Proceedings 6th Workshop on Mathematically Structured Functional Programming
Robert Atkey, Neelakantan Krishnaswami
The sixth workshop on Mathematically Structured Functional Programming is devoted to the derivation of functionality from structure. It is a celebration of the direct impact of The…