Travelled to:
1 × Canada
1 × China
1 × Denmark
1 × Italy
1 × Japan
1 × Poland
1 × Spain
1 × United Kingdom
2 × USA
Collaborated with:
∅ N.R.Krishnaswami B.Pientka F.Pfenning Y.Chen U.A.Acar Khurram A. Jafery M.A.Hammer K.Headley N.Labich J.S.Foster M.W.Hicks D.V.Horn
Talks about:
type (4) typecheck (3) polymorph (3) program (3) intersect (2) increment (2) bidirect (2) complet (2) higher (2) elabor (2)
Person: Joshua Dunfield
DBLP: Dunfield:Joshua
Contributed to:
Wrote 13 papers:
- ICFP-2015-Dunfield #morphism #polymorphism
- Elaborating evaluation-order polymorphism (JD), pp. 256–268.
- OOPSLA-2015-HammerDHLFHH #incremental
- Incremental computation with names (MAH, JD, KH, NL, JSF, MWH, DVH), pp. 748–766.
- ICFP-2013-DunfieldK #bidirectional #morphism #polymorphism #rank
- Complete and easy bidirectional typechecking for higher-rank polymorphism (JD, NRK), pp. 429–442.
- ICFP-2012-Dunfield
- Elaborating intersection and union types (JD), pp. 17–28.
- PLDI-2012-ChenDA #automation
- Type-directed automatic incrementalization (YC, JD, UAA), pp. 299–310.
- ICFP-2011-ChenDHA #functional #self #source code
- Implicit self-adjusting computation for purely functional programs (YC, JD, MAH, UAA), pp. 129–141.
- IJCAR-2010-PientkaD #deduction #framework #named #programming #reasoning
- Beluga: A Framework for Programming and Reasoning with Deductive Systems (BP, JD), pp. 15–21.
- PPDP-2008-PientkaD #programming #proving
- Programming with proofs and explicit contexts (BP, JD), pp. 163–173.
- POPL-2004-DunfieldP #bidirectional
- Tridirectional typechecking (JD, FP), pp. 281–292.
- FoSSaCS-2003-DunfieldP #call-by
- Type Assignment for Intersections and Unions in Call-by-Value Languages (JD, FP), pp. 250–266.
- ESOP-2017-Dunfield
- Extensible Datasort Refinements (JD), pp. 476–503.
- POPL-2017-JaferyD #nondeterminism
- Sums of uncertainty: refinements go gradual (KAJ, JD), pp. 804–817.
- POPL-2019-DunfieldK #bidirectional #morphism #polymorphism #rank
- Sound and complete bidirectional typechecking for higher-rank polymorphism with existentials and indexed types (JD, NRK), p. 28.