POPLmark Challenge via De Bruijn Indices

Stefan Berghofer 🌐

August 2, 2007

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

We present a solution to the POPLmark challenge designed by Aydemir et al., which has as a goal the formalization of the meta-theory of System F<:. The formalization is carried out in the theorem prover Isabelle/HOL using an encoding based on de Bruijn indices. We start with a relatively simple formalization covering only the basic features of System F<:, and explain how it can be extended to also cover records and more advanced binding constructs.

License

BSD License

Topics

Session POPLmark-deBruijn