@incollection{Her:05,
  volume = {3634},
  title = {Light functional interpretation: an optimization of {G}\"odel's
           technique towards the extraction of (more) efficient programs from
           (classical) proofs},
  year = {2005},
  booktitle = {Computer science logic},
  pages = {477--492},
  publisher = {Springer},
  address = {Berlin},
  author = {Hernest, Mircea-Dan},
  series = {Lecture Notes in Comput. Sci.},
}