Encoding Functional Relations in Scunak

We describe how a set-theoretic foundation for mathematics can be encoded in the new system Scunak. We then discuss an encoding of the construction of functions as functional relations in untyped set theory. Using the dependent type theory of Scunak, we can define obel application and lambda abstraction operators (in the spirit of higher-order abstract syntax) mediating between functions in the (metalevel) type theory and (object-level) functional relations. The encoding has also been exported to Automath and Twelf.

• Type: Journal
• Year: 2007
• Where: ENTCS
• Authors: Chad E. Brown
• Keywords: Dependent Type Theory, ENTCS 2007, Functional Relations, Type Theory