FLOC 2018: FEDERATED LOGIC CONFERENCE 2018
Theories as Types

Authors: Dennis Müller, Florian Rabe and Michael Kohlhase

Paper Information

Title:Theories as Types
Authors:Dennis Müller, Florian Rabe and Michael Kohlhase
Proceedings:IJCAR Proceedings 9th IJCAR, 2018
Editors: Stephan Schulz, Didier Galmiche and Roberto Sebastiani
Keywords:type theory, record types, theories, models
Abstract:

ABSTRACT. Theories are an essential structuring principle that enable modularity, encapsulation, and reuse in formal libraries and programs (called classes there). Similar effects can be achieved by dependent record types. While the former forms a separate language layer, the latter is a normal part of the type theory. This overlap in functionality can render different systems non-interoperable and lead to duplication of work.

We present a type-theoretic calculus and implementation of a variant of record types that for a wide class of formal languages naturally corresponds to theories. Moreover, we can now elegantly obtain a contravariant functor that reflects the theory level into the object level: for each theory we obtain the type of its models and for every theory morphism a function between the corresponding types. In particular this allows shallow – and thus structure-preserving – encodings of mathematical knowledge and program specifications while allowing the use of object-level features on models, e.g. equality and quantification.

Pages:16
Talk:Jul 15 17:30 (Session 107D: Logics, Frameworks and Proofs)
Paper: