Synthetic Tait Computability the Hard Way
Logic in Computer Science
2023-10-04 v1
Abstract
We walk through a few proofs of canonicity and normalization, each one with more aspects dissected and re-expressed in category theory, so that readers can compare the difference across proofs. During this process we isolate the different ideas that make up the proofs. Finally we arrive at synthetic Tait computability as proposed by J. Sterling. We also give a synthetic proof for parametricity of system F.
Keywords
Cite
@article{arxiv.2310.02051,
title = {Synthetic Tait Computability the Hard Way},
author = {Xu Huang},
journal= {arXiv preprint arXiv:2310.02051},
year = {2023}
}
Comments
73 pages, A5 paper, optimized for phone viewing