An implementation of a dependent type theory with uniqueness types and types for runtime erasure.
- https://personal.cis.strath.ac.uk/conor.mcbride/PlentyO-CR.pdf
- https://link.springer.com/content/pdf/10.1007/978-3-030-99336-8.pdf
- https://www.researchgate.net/profile/Rinus-Plasmeijer-2/publication/221600600_Uniqueness_Typing_Simplified/links/0046352262ddf9e694000000/Uniqueness-Typing-Simplified.pdf?origin=publication_detail