Values, Types and Foundations

I took the opportunity to step out for the first time in quite a while and present Values, Types and Foundations at the Object Management Group’s (OMG) September Technical Meeting. Many thanks to my friends there, especially Larry Johnson and John Butler, Co-Chairs of the GovDTF, for the opportunity to do so.

Values, Types and Foundations is a broad survey presentation and demonstration. The presentation very generally describes a theoretical foundation for OMG standards such as the Meta Object Facility and the Object Constraint Language. By general I mean a computational, logical and philosophical overview through System F, the Calculus of Constructions, Martin-Lof Type Theory and dependent types. My goal was to give the talk that Philip Wadler would give to the OMG. The presentation also contains an informational brief on Vladimir Voevodsky’s Univalent Foundations program at the Institute for Advanced Studies.

The first four demonstrations use most of Oleg Kiseylov’s Interpreting Types as Abstract Values, Constructive Law of Excluded Middle, and Impredicativity Bites. I don’t add much of anything new to the demos. I compare and contrast the test cases Oleg provides and dump the stack traces to speed up the demonstration time. That’s way more than enough.

The last demonstration is based on Anton Setzer’s Interactive Theorem Proving for Agda Users.

Other than that I review some background on Types, Classes and Sets based on Peter Aczel’s What is a Set? Thanks to Cory Casanave for pointing out the importance of providing this background.

During the voice over and at the conference I contrasted the approach in Values, Types and Foundations with that of ISO 24707 Common Logic (CL) which is a type free logic. Pat Hayes describes CL as first order syntax and higher order semantics. Hmmm. I recommend Chris Menzel’s  Knowledge Representation, the World Wide Web and the Evolution of Logic for those  interested in the design goals that motivated ISO 24707.

I plan to step out a bit more in 2012. I will be connecting Values, Types and Foundations back to some topics I wrote about here on the Phaneron a few years ago such as  the Heterogeneous Tool Set and the Information Flow Framework. The wood shedding has paid off and I’m looking forward to catching up with a few old friends and mixing it up with some new folks.