# 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. BibTeX: @article{POPLmark-deBruijn-AFP, author = {Stefan Berghofer}, title = {POPLmark Challenge Via de Bruijn Indices}, journal = {Archive of Formal Proofs}, month = aug, year = 2007, note = {\url{https://isa-afp.org/entries/POPLmark-deBruijn.html}, Formal proof development}, ISSN = {2150-914x}, } License: BSD License