## AbstractBidirectional 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 ( |

- Paper (27 pages)
- Omitted definitions and proofs (188 pages)

@Unpublished{Dunfield18:gadts, author = {Joshua Dunfield and Neelakantan R. Krishnaswami}, title = {Sound and Complete Bidirectional Typechecking for Higher-Rank Polymorphism with Existentials and Indexed Types}, month = jul, year = {2018}, note = {\url{http://arxiv.org/abs/1601.05106}} }

all papers * related papers

Joshua Dunfield