Dependent type systems as macros

Stephen Chang; Michael Ballantyne; Milo Turner; William J. Bowman

doi:10.1145/3371071

Dependent type systems as macros

Stephen Chang
, Michael Ballantyne
, Milo Turner
, William J. Bowman

Computer Science

Research output: Contribution to journal › Article › peer-review

Original language	English
Article number	3
Journal	Proceedings of the ACM on Programming Languages
Volume	4
Issue number	POPL
DOIs	https://doi.org/10.1145/3371071
State	Published - Jan 2020

ASJC Scopus Subject Areas

Software
Safety, Risk, Reliability and Quality

Keywords

Dependent types
Macros
Proof assistants
Type systems

Access to Document

10.1145/3371071

Cite this

@article{cbab627c264c451085f49f678a86be5b,

title = "Dependent type systems as macros",

keywords = "Dependent types, Macros, Proof assistants, Type systems",

author = "Stephen Chang and Michael Ballantyne and Milo Turner and Bowman, \{William J.\}",

year = "2020",

month = jan,

doi = "10.1145/3371071",

language = "English",

volume = "4",

journal = "Proceedings of the ACM on Programming Languages",

issn = "2475-1421",

publisher = "Association for Computing Machinery (ACM)",

number = "POPL",

}

TY - JOUR

T1 - Dependent type systems as macros

AU - Chang, Stephen

AU - Ballantyne, Michael

AU - Turner, Milo

AU - Bowman, William J.

PY - 2020/1

Y1 - 2020/1

KW - Dependent types

KW - Macros

KW - Proof assistants

KW - Type systems

UR - https://www.scopus.com/pages/publications/85088260337

UR - https://www.scopus.com/pages/publications/85088260337#tab=citedBy

U2 - 10.1145/3371071

DO - 10.1145/3371071

M3 - Article

AN - SCOPUS:85088260337

SN - 2475-1421

VL - 4

JO - Proceedings of the ACM on Programming Languages

JF - Proceedings of the ACM on Programming Languages

IS - POPL

M1 - 3

ER -

Dependent type systems as macros

ASJC Scopus Subject Areas

Keywords

Access to Document

Other files and links

Fingerprint

Cite this