HackerPapers

arXiv:2210.08232cs.PL

A tutorial on implementing De Morgan cubical type theory

Tesla Zhang

Early discovery. Linked by one identifiable commenter. This paper is outside the main ranking; a mention is not an endorsement.

Abstract

This tutorial explains (one way) how to implement De Morgan cubical type theory to people who know how to implement a dependent type theory. It contains an introduction to basic concepts of cubes, type checking algorithms under a cofibration, the idea of "transportation rules" and cubical operations. This tutorial is a by-product of an experimental implementation of cubical type theory, called Guest0x0.

arXiv comments
27 pages
Journal reference
DOI
Subjects
cs.PLProgramming Languages

On Hacker News

Linked by 1 identifiable commenter in 1 comment across 1 thread, from Oct 2023 to Oct 2023.

Comments linking this paper, per year.

Discussed in comments1 thread

  1. The deep link equating math proofs and computer programs 1 comment

    • It should be possible to embed cubical type theory in Idris.[1][2] 1: https://arxiv.org/abs/2210.08232 2: https://chat.openai.com/share/aadb7a0a-08a4-4951-b877-cb2f61...

      haltistView on HNParent context

Submitted to Hacker News

Connected through shared HN threads, not inferred similarity or a recommendation.