
Our preferred starting point is the formalisation of set theory in Higher Order Logic.
This provides a universal semantic foundation for XLogic, and a suitable framework for further formal foundational experiments.

Some experiments in foundation systems intended to deliver pragmatic features like polymorhphism and structured namespaces without rocking the boat.


The identification of functions with wellfounded graphs is both fruitful and cumbersome.
Is it possible to reconcile this classical framework with a more liberal notion of "rule"?

Formal foundation systems are normally associated with fixed sets of rules and axioms.
For XLogic, liberalisation is proposed, yielding a closer relationship between proof and computation.

The attempt to define semantics formally leads either to infinite regress or to metacircular semantics.
We propose the latter.

