Type Systems and Verifiable Guarantees
Veritas is a workbench for simplifying the development of sound type systems. Veritas provides a single, high-level specification language for type systems, from which it automatically tries to derive soundness proofs and efficient and correct type-checking algorithms. |
A type checker has an important role to ensure that programs exhibit a desired behavior. It uses the typing context to coordinate type checking from different subexpression of the typing derivation, therefore
dependencies are build between subexpressions. These dependencies prevent the type checker to be incremental.
We propose an extension of co-contextual type checking to support Featherweight Java. Co-contextualizing type rules is a technique for constructing type systems that are easy to be incremental. To co-contextualize Featherweight Java we eliminate the context and the class table, where Featherweight Java for type checking uses a typing context and a class table, and replace them by a different structure. As a result, eliminating the context and the class table, and having co-contextual formulation of type rules, we remove the unnecessary dependencies between subexpressions, and facilitate the Featherweight Java type system to be incremental. We describe a method to construct co-contextual type rules, from constraint-based type rules for Featherweight Java. We have an implementation of co-contextual Featherweight Java type, use cases and as well a theorem as proof of equivalence between Featherweight Java and co-contextual Featherweight Java type systems.