A Dependently Typed Language with Dynamic Equality

Reference. A Dependently Typed Language with Dynamic Equality

Mark Lemay, Qiancheng Fu, William Blair, Cheng Zhang, Hongwei Xi · TyDe · 2023 · type-theory · DOI

Cite

Cite as @lemay-2023-a (helia, typst) · \cite{lemay-2023-a} (LaTeX)

BibTeX

bibtex · 1 line

@inproceedings{lemay-2023-a, series={TyDe ’23}, title={A Dependently Typed Language with Dynamic Equality}, url={http://dx.doi.org/10.1145/3609027.3609407}, DOI={10.1145/3609027.3609407}, booktitle={Proceedings of the 8th ACM SIGPLAN International Workshop on Type-Driven Development}, publisher={ACM}, author={Lemay, Mark and Fu, Qiancheng and Blair, William and Zhang, Cheng and Xi, Hongwei}, year={2023}, month=Aug, pages={44–57} }

hayagriva YAML (typst)

yaml · 21 lines

lemay-2023-a:
  type: article
  title: A Dependently Typed Language with Dynamic Equality
  author:
  - Lemay, Mark
  - Fu, Qiancheng
  - Blair, William
  - Zhang, Cheng
  - Xi, Hongwei
  date: 2023-08
  page-range: 44-57
  url: http://dx.doi.org/10.1145/3609027.3609407
  serial-number:
    doi: 10.1145/3609027.3609407
  parent:
    type: proceedings
    title: Proceedings of the 8th ACM SIGPLAN International Workshop on Type-Driven Development
    publisher: ACM
    parent:
      type: proceedings
      title: TyDe ’23

Download: lemay-2023-a.bib · lemay-2023-a.yml

Cites 37 works (2 here)

With notes (2)

Bidirectional Typing dunfield-2021-bidirectionalACM Computing Surveys · 2021

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. Using checking enables bidirectional typing to support features for which inference is undecidable; using synthesis enables bidirectional typing to avoid the large annotation burden of explicitly typed languages. In addition, bidirectional typing improves error locality. We highlight the design principles that underlie bidirectional type systems, survey the development of bidirectional typing from the prehistoric period before Pierce and Turner’s local type inference to the present day, and provide guidance for future investigations.

DOI · arXiv

Elimination with a Motive mcbride-2002-eliminationTYPES · 2002

DOI

External (35)

Gradualizing the Calculus of Inductive Constructions (2020)
Programming Language Foundations in Agda (2020)
λdB: Blame tracking at higher fidelity (2020)
Approximate normalization for gradual dependent types (2019)
Theorems for free for free: parametricity, with and without types (2017)
Gradual refinement types (2017)
Dependent types in haskell: Theory and practice (2016)
Abstracting gradual typing (2016)
Autosubst: Reasoning with de Bruijn Terms and Parallel Substitutions (2015)
Refined Criteria for Gradual Typing (2015)
Programming up to Congruence (2015)
A Complement to Blame (2015)
Irrelevance, heterogeneous equality, and call-by-value dependent type systems (2012)
Equality proofs and deferred type errors: a compiler pearl (2012)
ΠΣ: Dependent Types without the Sugar (2010)
Dependent types and program equivalence (2010)
Hybrid type checking (TOPLAS) (2010)
Compositional reasoning and decidable checking for dependent contract types (2009)
Well-Typed Programs Can't Be Blamed (2009)
Gradual Typing for Objects (2007)
Dependent ML An approach to practical programming with dependent types (2007)
Hybrid type checking (2006)
Interlanguage migration (2006)
Dynamic Typing with Dependent Types (2004)
Contracts for higher-order functions (2002)
An Implementation of Type: Type (2000)
Dependently typed functional programs and their proofs (PhD thesis) (2000)
Cayenne—a language with dependent types (1998)
An Algorithm for Type-Checking Dependent Types (1996)
A Syntactic Approach to Type Soundness (1994)
Domain Interpretations of Martin-Löf's Partial Type Theory (1990)
A Polymorphic λ-calculus with Type:Type (DEC SRC report) (1986)
Towards a theory of type structure (1974)
An intuitionistic theory of types (1972)
Towards a practical programming language based on dependent type theory. Ph. D. Dissertation. Department of Computer Science and Engineering