Skip to main content
PRL Project

Representing Red-Black Trees in MetaPRL

by Alexei Kopylov
2002-2003

I'll show how we can define abstract data structures such as Set and Table in MetaPRL using depnedend records, and implement such structures using binary trees and red-black trees.

I faced some unexpected problems connecting with functionality and recursive types.

It turns out that Nuprl rules for recursive type are invalid and lead to contradiction!