59 citations · 92 across the 9 of their papers we have counts for
11 papers
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…
flap: A Deterministic Parser with Fused Lexing
Jeremy Yallop, Ningning Xie, Neel Krishnaswami
Lexers and parsers are typically defined separately and connected by a token stream. This separate definition is important for modularity and reduces the potential for parsing ambi…
Focusing on Refinement Typing
Dimitrios J. Economou, Neel Krishnaswami, Jana Dunfield
We present a logically principled foundation for systematizing, in a way that works with any computational effect and evaluation order, SMT constraint generation seen in refinement…
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…
Bidirectional Typing
Jana Dunfield, Neel Krishnaswami
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.…