POPLmark Challenge Via de Bruijn Indices


Title: POPLmark Challenge Via de Bruijn Indices
Author: Stefan Berghofer
Submission date: 2007-08-02
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.
  author  = {Stefan Berghofer},
  title   = {POPLmark Challenge Via de Bruijn Indices},
  journal = {Archive of Formal Proofs},
  month   = aug,
  year    = 2007,
  note    = {\url{http://isa-afp.org/entries/POPLmark-deBruijn.shtml},
            Formal proof development},
  ISSN    = {2150-914x},
License: BSD License
Status: [ok] This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.