depsterr
/
pi
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
A typechecker for intensional MLTT without elaboration.
You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
34 Commits
1 Branch
0 Tags
912 KiB
 
 
Tag: Branch: Tree: master
Branches Tags
${ item.name }
Create tag ${ searchTerm }
Create branch ${ searchTerm }
from 'master'
${ noResults }
Rachel Samuelsson c7eac71a2d
update expectations in readme 		9 months ago
src align arrows 10 months ago
tests update readme 10 months ago
.gitignore initial commit 1 year ago
README.md update expectations in readme 9 months ago
makefile definition system, repl 10 months ago
pi.ipkg definition system, repl 10 months ago

README.md

pi

A dependently typed system

Implemented

  • A Basic dependent lambda calculus

    • lambda abstractions
    • variables
    • pi types
    • type of types

  • let … in …

  • Unit type

  • Empty type

  • Natural numbers

  • Σ Types

  • Martin-Löf Identity types

Lacking

Here are some things which are not present but could be.

This project has served me well by teaching me about typechecking dependently typed systems. It’s likely that the features listed below will not be implemented as I’ll move onto other projects and learn more about elaboration.

  • Universes
    • a la tarksi
  • Inductives
    • W types
    • Indexed inductives
  • Elaboration
    • Implicit arguments
    • Universe family application
      • Syntax level russel universes
      • Universe of all other universes? (universe polymorphism)

References

Some of the material I found helpful in groking dependent type checking: