Sciweavers

Share
ENTCS
2007

Encoding Functional Relations in Scunak

8 years 11 months ago
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.
Chad E. Brown
Added 13 Dec 2010
Updated 13 Dec 2010
Type Journal
Year 2007
Where ENTCS
Authors Chad E. Brown
Comments (0)
books