@book{LNCS2283,
  author={Tobias Nipkow and Lawrence Paulson and Markus Wenzel}, 
  title="Isabelle/HOL --- A Proof Assistant for Higher-Order Logic",
  publisher=Springer,series=LNCS,volume=2283,year=2002,
  note={\url{http://www.in.tum.de/~nipkow/LNCS2283/}}
}


@article{FJ,
 author = {Atsushi Igarashi and Benjamin C. Pierce and Philip Wadler},
 title = {Featherweight {J}ava: {A} minimal core calculus for {J}ava and {GJ}},
 journal = {ACM Transactions on Programming Languages and Systems},
 volume = {23},
 number = {3},
 year = {2001},
 issn = {0164-0925},
 pages = {396--450},
 doi = {http://doi.acm.org/10.1145/503502.503505},
 publisher = {ACM Press},
 address = {New York, NY, USA},
 }