With-Type – Poor man's dependent types

Dominique Unruh 🌐

August 29, 2024

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.

Abstract

The type system of Isabelle/HOL does not support dependent types or arbitrary quantification over types. We introduce a system to mimic dependent types and existential quantification over types in limited circumstances at the top level of theorems.

License

BSD License

Topics

Session With_Type