59 citations · 106 across the 9 of their papers we have counts for
12 papers
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…
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.…
Fungi: Typed incremental computation with names
Matthew A. Hammer, Jana Dunfield, Kyle Headley +2
Incremental computations attempt to exploit input similarities over time, reusing work that is unaffected by input changes. To maximize this reuse in a general-purpose programming…
Extensible Datasort Refinements
Jana Dunfield
Refinement types turn typechecking into lightweight verification. The classic form of refinement type is the datasort refinement, in which datasorts identify subclasses of inductiv…
Sums of Uncertainty: Refinements Go Gradual
Khurram A. Jafery, Jana Dunfield
A long-standing shortcoming of statically typed functional languages is that type checking does not rule out pattern-matching failures (run-time match exceptions). Refinement types…
Refinement types for precisely named cache locations
Matthew A. Hammer, Jana Dunfield, Dimitrios J. Economou +1
Many programming language techniques for incremental computation employ programmer-specified names for cached information. At runtime, each name identifies a "cache location" for a…
Sound and Complete Bidirectional Typechecking for Higher-Rank Polymorphism with Existentials and Indexed Types
Jana Dunfield, Neelakantan R. Krishnaswami
Bidirectional typechecking, in which terms either synthesize a type or are checked against a known type, has become popular for its applicability to a variety of type systems, its…
Elaborating Evaluation-Order Polymorphism
Jana Dunfield
We classify programming languages according to evaluation order: each language fixes one evaluation order as the default, making it transparent to program in that evaluation order,…
Incremental Computation with Names
Matthew A. Hammer, Jana Dunfield, Kyle Headley +4
Over the past thirty years, there has been significant progress in developing general-purpose, language-based approaches to incremental computation, which aims to efficiently updat…
Annotations for Intersection Typechecking
Jana Dunfield
In functional programming languages, the classic form of annotation is a single type constraint on a term. Intersection types add complications: a single term may have to be checke…
Complete and Easy Bidirectional Typechecking for Higher-Rank Polymorphism
Jana Dunfield, Neelakantan R. Krishnaswami
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,…
Untangling Typechecking of Intersections and Unions
Jana Dunfield
Intersection and union types denote conjunctions and disjunctions of properties. Using bidirectional typechecking, intersection types are relatively straightforward, but union type…