@article{Berardi-Tatsuta/12,
AUTHOR = {Berardi, Stefano and Tatsuta, Makoto},
TITLE = {Internal models of system F for decompilation},
JOURNAL = {Theor.~Comput.~Sci.},
VOLUME = {435},
PAGES = {3-20},
YEAR = {2012},
EDITOR = {Ausiello, G. and Sannella, D.},
KEYWORDS = {typed $\lambda$ -calculus, system f, semantics of polymorphism, compiler, decompiler, de bruijn level},
URL = {http://www.sciencedirect.com/science/article/pii/S0304397512001636},
PUBLISHER = {Elsevier B.V.},
ADDRESS = {Amsterdam-Boston-London-New York-Oxford-Paris-Philadelphia-San Diego-St. Louis},
}
@article{Danvy-Millikin-Munk-Zerny/12,
AUTHOR = {Danvy, Olivier and Millikin, Kevin and Munk, Johan and Zerny, Ian},
TITLE = {On inter-deriving small-step and big-step semantics: A case study for storeless call-by-need evaluation},
JOURNAL = {Theor.~Comput.~Sci.},
VOLUME = {435},
PAGES = {21-42},
YEAR = {2012},
EDITOR = {Ausiello, G. and Sannella, D.},
URL = {http://www.sciencedirect.com/science/article/pii/S0304397512001648},
PUBLISHER = {Elsevier B.V.},
ADDRESS = {Amsterdam-Boston-London-New York-Oxford-Paris-Philadelphia-San Diego-St. Louis},
}
@article{Howe-King/12,
AUTHOR = {Howe, Jacob M. and King, Andy},
TITLE = {A pearl on SAT and SMT solving in Prolog},
JOURNAL = {Theor.~Comput.~Sci.},
VOLUME = {435},
PAGES = {43-55},
YEAR = {2012},
EDITOR = {Ausiello, G. and Sannella, D.},
KEYWORDS = {sat solving, smt solving, prolog, constraint logic programming},
URL = {http://www.sciencedirect.com/science/article/pii/S030439751200165X},
PUBLISHER = {Elsevier B.V.},
ADDRESS = {Amsterdam-Boston-London-New York-Oxford-Paris-Philadelphia-San Diego-St. Louis},
}
@article{Kiselyov/12,
AUTHOR = {Kiselyov, Oleg},
TITLE = {Delimited control in OCaml, abstractly and concretely},
JOURNAL = {Theor.~Comput.~Sci.},
VOLUME = {435},
PAGES = {56-76},
YEAR = {2012},
EDITOR = {Ausiello, G. and Sannella, D.},
KEYWORDS = {delimited continuation, exception, semantics, implementation, abstract machine},
URL = {http://www.sciencedirect.com/science/article/pii/S0304397512001661},
PUBLISHER = {Elsevier B.V.},
ADDRESS = {Amsterdam-Boston-London-New York-Oxford-Paris-Philadelphia-San Diego-St. Louis},
}
@article{Remy-Yakobowski/12,
AUTHOR = {R{\'e}my, Didier and Yakobowski, Boris},
TITLE = {A church-style intermediate language for MLF},
JOURNAL = {Theor.~Comput.~Sci.},
VOLUME = {435},
PAGES = {77-105},
YEAR = {2012},
EDITOR = {Ausiello, G. and Sannella, D.},
KEYWORDS = {mlf, systemf, types, type generalization, type instantiation, retyping functions, coercions, type soundness, binders},
URL = {http://www.sciencedirect.com/science/article/pii/S0304397512001673},
PUBLISHER = {Elsevier B.V.},
ADDRESS = {Amsterdam-Boston-London-New York-Oxford-Paris-Philadelphia-San Diego-St. Louis},
}
@article{Saurin/12,
AUTHOR = {Saurin, Alexis},
TITLE = {B{\"o}hm theorem and B{\"o}hm trees for the $\Lambda\mu$-calculus},
JOURNAL = {Theor.~Comput.~Sci.},
VOLUME = {435},
PAGES = {106-138},
YEAR = {2012},
EDITOR = {Ausiello, G. and Sannella, D.},
KEYWORDS = {$\lambda$ $\mu$ -calculus, b{\"o}hm theorem, b{\"o}hm trees, classical $\lambda$ -calculi, (delimited) control, infinitary $\lambda$ -calculus, separation property, shift/reset, streams},
URL = {http://www.sciencedirect.com/science/article/pii/S0304397512001685},
PUBLISHER = {Elsevier B.V.},
ADDRESS = {Amsterdam-Boston-London-New York-Oxford-Paris-Philadelphia-San Diego-St. Louis},
}