@InProceedings{	  wolff:verifying:2001,
  abstract	= {Binding structures enrich traditional abstract syntax by
		  provi-ding support for representing binding mechanisms
		  (based on deBruijn indices), term-schemata and a very clean
		  algebraic theory of substitution. Weprovide a novel binding
		  structure with the following main results: 1) The
		  formalisation of a generic binding structure with the novel
		  conceptof effect-binding that enables the explicit
		  representations of both contexts and terms inside one term
		  meta-language,2) The foundation of a formal
		  (machine-assisted) substitution theory of effect-binding
		  that is well-suited for mechanisation. This can be used for
		  thesystematic and correct development of new calculi with
		  explicit substitutions.The substitution theory is formally
		  proven in Isabelle/HOL; the implementation may serve as
		  (untyped) framework for deep embeddings.},
  author	= {Burkhart Wolff},
  classification= {proceedings},
  booktitle	= {Workshop on Explicit Substitution Theory and Applications
		  (WESTAPP'01)},
  editor	= {Pierre Lescanne},
  isbn		= {90-393-2764-5},
  language	= {english},
  month		= {May},
  pages		= {58 -- 71},
  ps		= {papers/2001/BiSE.ps.gz},
  publisher	= {Department of Philosophy - Utrecht University},
  series	= {Logic Group Preprint Series},
  title		= {Verifying Explicit Substitution Calculi in Binding
		  Structures with Effect Binding},
  volume	= 210,
  year		= 2001
}

@InProceedings{	  wolff:verifying:2001,
  abstract	= {Binding structures enrich traditional abstract syntax by
		  provi-ding support for representing binding mechanisms
		  (based on deBruijn indices), term-schemata and a very clean
		  algebraic theory of substitution. Weprovide a novel binding
		  structure with the following main results: 1) The
		  formalisation of a generic binding structure with the novel
		  conceptof effect-binding that enables the explicit
		  representations of both contexts and terms inside one term
		  meta-language,2) The foundation of a formal
		  (machine-assisted) substitution theory of effect-binding
		  that is well-suited for mechanisation. This can be used for
		  thesystematic and correct development of new calculi with
		  explicit substitutions.The substitution theory is formally
		  proven in Isabelle/HOL; the implementation may serve as
		  (untyped) framework for deep embeddings.},
  author	= {Burkhart Wolff},
  classification= {proceedings},
  booktitle	= {Workshop on Explicit Substitution Theory and Applications
		  (WESTAPP'01)},
  editor	= {Pierre Lescanne},
  isbn		= {90-393-2764-5},
  language	= {english},
  month		= {May},
  pages		= {58 -- 71},
  ps		= {papers/2001/BiSE.ps.gz},
  publisher	= {Department of Philosophy - Utrecht University},
  series	= {Logic Group Preprint Series},
  title		= {Verifying Explicit Substitution Calculi in Binding
		  Structures with Effect Binding},
  volume	= 210,
  year		= 2001
}