📧mail: jcxz@seas.upenn.edu
ORCID: 0000-0003-0830-3180

Education

University of Pennsylvania, Philadelphia, PA, USA
PhD in Computer and Information Science, ongoing
Advisor: Stephanie Weirich

University of British Columbia, Vancouver, BC, Canada
MSc. in Computer Science, November 2022
Advisor: William J. Bowman
Sized Dependent Types via Extensional Type Theory
[Thesis] [GitHub] [Slides]

@mastersthesis{STT,
  author = {Chan, Jonathan},
  title = {{Sized Dependent Types via Extensional Type Theory}},
  school = {University of British Columbia},
  address = {Vancouver, BC, Canada},
  url = {https://open.library.ubc.ca/soa/cIRcle/collections/ubctheses/24/items/1.0416401},
  doi = {10.14288/1.0416401},
  year = {2022},
  month = jul,
  key = {STT}
}

University of British Columbia, Vancouver, BC, Canada
BSc. Combined Honours in Computer Science and Physics, May 2020
Advisor: William J. Bowman
Practical Sized Typing for Coq
[Thesis] [GitHub] [Proposal]

@mastersthesis{PSTC,
  author = {Chan, Jonathan},
  title = {{Practical Sized Typing for Coq}},
  school = {University of British Columbia},
  address = {Vancouver, BC, Canada},
  url = {https://open.library.ubc.ca/collections/undergraduateresearch/52966/items/1.0406074},
  doi = {10.14288/1.0406074},
  year = {2019},
  month = dec,
  type = {Bachelor's thesis},
  key = {PSTC}
}

Drafts and Publications

Bounded First-Class Universe Levels in Dependent Type Theory
Jonathan Chan and Stephanie Weirich
Rejected from FSCD 2025
[Manuscript] [arXiv]

@unpublished{TTBFL,
  author = {Chan, Jonathan and Weirich, Stephanie},
  title = {{Bounded First-Class Universe Levels in Dependent Type Theory}},
  year = {2025},
  url = {https://arxiv.org/abs/2502.20485},
  doi = {10.48550/arXiv.2502.20485},
  key = {TTBFL}
}

Stratified Type Theory
Jonathan Chan and Stephanie Weirich
Programming Languages and Systems, LNCS 15694(ESOP), May 2025
Presented at NJPLS 2023 @ Princeton University
[ESOP 2025] [GitHub] [Artifact] [Slides] [FSCD 2024 draft] [CPP 2024 draft]

@inproceedings{StraTT,
  author = {Chan, Jonathan and Stephanie, Weirich},
  editor = {Vafeiadis, Viktor},
  title = {{Stratified Type Theory}},
  booktitle = {Programming Languages and Systems},
  publisher = {Springer Cham},
  year = {2025},
  pages = {236--263},
  doi = {10.1007/978-3-031-91118-7\_10},
  key = {StraTT}
}

Consistency of a Dependent Calculus of Indistinguishability
Yiyun Liu, Jonathan Chan, and Stephanie Weirich
Proceedings of the ACM on Programming Languages, 9(POPL), January 2025
[PACMPL] [POPL 2025] [Artifact]

@article{DCOIω,
  author = {Liu, Yiyun and Chan, Jonathan and Weirich, Stephanie},
  title = {{Consistency of a Dependent Calculus of Indistinguishability}},
  year = {2025},
  publisher = {Association for Computing Machinery},
  volume = {9},
  number = {POPL},
  url = {https://doi.org/10.1145/3704843},
  doi = {10.1145/3704843},
  journal = {Proc. ACM Program. Lang.},
  month = jan,
  articleno = {7},
  numpages = {27},
  pages = {183--209},
  key = {DCOIω}
}

Internalizing Extensions in Lattices of Type Theories
Jonathan Chan
CIS research qualifier @ UPenn, 21 November 2024
[Report] [Slides]

Internalizing Indistinguishability with Dependent Types
Yiyun Liu, Jonathan Chan, Jessica Shi, and Stephanie Weirich
Proceedings of the ACM on Programming Languages, 8(POPL), January 2024
[PACMPL] [POPL 2024] [Artifact]

@article{DCOI,
  author = {Liu, Yiyun and Chan, Jonathan and Shi, Jessica and Weirich, Stephanie},
  title = {{Internalizing Indistinguishability with Dependent Types}},
  year = {2024},
  publisher = {Association for Computing Machinery},
  volume = {8},
  number = {POPL},
  url = {https://doi.org/10.1145/3632886},
  doi = {10.1145/3632886},
  journal = {Proc. ACM Program. Lang.},
  month = jan,
  articleno = {44},
  numpages = {28},
  pages = {1298--1325},
  key = {DCOI}
}

Is Sized Typing for Coq Practical?
Jonathan Chan, Yufeng (Michael) Li, and William J. Bowman
Journal of Functional Programming, 33(e1), January 2023
[JFP] [ICFP 2023] [arXiv] [GitHub] [Artifact] [POPL 2021 draft] [CPP 2020 draft]

@article{ISTCP,
  title = {{Is sized typing for Coq practical?}},
  volume = {33},
  doi = {10.1017/S0956796822000120},
  journal = {Journal of Functional Programming},
  publisher = {Cambridge University Press},
  author = {Chan, Jonathan and Li, Yufeng and Bowman, William J.},
  year = {2023},
  month = jan,
  pages = {e1},
  key = {ISTCP}
}

Towards a Syntactic Model of Sized Dependent Types
Jonathan Chan
3^rd place finalist at the Student Research Competition @ POPL 2022
[Abstract] [Video + Slides] [Slides (draft)]

@misc{SRC,
  title = {{Towards a Syntactic Model of Sized Dependent Types}},
  author = {Chan, Jonathan},
  url = {https://popl22.sigplan.org/details/POPL-2022-student-research-competition/1/Towards-a-Syntactic-Model-of-Sized-Dependent-Types},
  year = {2022},
  month = jan,
  key = {SRC}
}

Other Papers, Talks, and Presentations

Strong Normalization for Call-by-Push-Value
CIS 6700 (Spring 2025) final project
[Report] [GitHub]

Paradoxes in Type Theory
presented at PLClub @ UPenn
[4 April 2025]

ergonomics of PL metatheory in Lean
presented at PLClub @ UPenn
[7 June 2024]

quizzo
[12 June 2023] [13 March 2023]

Silence of the Vowels
presented at UDLS @ UBC
[22 October 2021]

Teaching Assistantships

University of Pennsylvania

University of British Columbia

Conferences

Other Service and Work

types.pl, Mastodon instance
Coädministrator and comoderator with @haskal (and formerly Tulip)
23 October 2020 – present

PLClub, University of Pennsylvania, Philadelphia, PA, USA
Coörganizer with Cassia Torczon
November 2023 – December 2024

Digital Health Innovation Lab, BC Children’s Hospital, Vancouver, BC, Canada
Software Programmer Co-op
May – August 2018

• Contributed to LambdaNative, an open-source cross-platform app framework written in Gambit Scheme
• Added features to LambdaNative apps RRate and ShareVitalSigns
• Cared for and nurtured the avocado seed growing on the windowsill in the lunch room

Visier Inc., Vancouver, BC, Canada
Software Developer Co-op
May – December 2017

• Improved developer tools and workflows in the Frameworks and Enablement team
• Created a proof-of-concept for migrating codebase from Mercurial to Git and designed a custom Gitflow workflow
• Incorporated automated endpoint documentation generation in Scala backend codebase
• Helped improve Angular web app compile/load times and modularity

Paragon Testing Enterprises, Vancouver, BC, Canada
Junior Software Developer and Quality Assurance Intern
January – August 2016

• Wrote a pilot test delivery application in WinForms for R&D to test and validate the design of the new CAEL computerized exam
• Refactored web app test scripts
• Participated in Paragon’s volleyball team for the Broadway Tech Centre’s volleyball tournament

Scholarships and Awards

George M. Ball, Jr. Fellowship (UPenn), 2022
Donor-named fellowships like these provide a one-time $3,000 award, which will be offered to you in the middle of your first semester upon enrollment. This honor and award is in recognition of your outstanding academic accomplishments and research potential.

British Columbia Graduate Scholarship (declined) (UBC), 2022
The province of British Columbia has funded BC Graduate Scholarships (BCGS) in any field of study, with emphasis on research in science, technology, engineering and mathematics (STEM) fields, and support for Indigenous students. The scholarships of $15,000 will be awarded by graduate programs and disciplinary Faculties.

Canada Graduate Scholarship – Master’s, 2021
[Outline of proposed research]
The objective of the Canada Graduate Scholarships – Master’s (CGS M) program is to help develop research skills and assist in the training of highly qualified personnel by supporting students who demonstrate a high standard of achievement in undergraduate and early graduate studies.

CRA Outstanding Undergraduate Researcher Award Honourable Mention, 2020
[Research summary]
This award program recognizes undergraduate students in North American colleges and universities who show outstanding potential in an area of computing research.

Dean of Science Scholarship (UBC), 2018, 2015
The Dean of Science Scholarship honours the most promising science undergraduate students and are made on the recommendation of the Faculty.

Trek Excellence Scholarship for Continuing Students (UBC), 2018, 2016, 2015
Trek Excellence Scholarships are offered every year to students in the top 5% of their undergraduate year, faculty, and school.

Charles and Jane Banks Scholarship (UBC), 2019, 2017
Scholarships are awarded on the recommendation of the Faculty of Science, to students who have completed at least one year, and are continuing in an undergraduate program.

J. Fred Muir Memorial Scholarship in Science (UBC), 2016
The awards are offered to students in the Faculty of Science on the recommendation of the Faculty.