Abstract is missing.
- Reasoning about recursive procedures with parametersRalph-Johan Back, Viorel Preoteasa. [doi]
- Verifying CPS transformations in Isabelle/HOLYasuhiko Minamide, Koji Okuma. [doi]
- Explicit substitutions and higher-order syntaxNeil Ghani, Tarmo Uustalu. [doi]
- Reasoning on an imperative object-based calculus in Higher Order Abstract SyntaxAlberto Ciaffaglione, Luigi Liquori, Marino Miculan. [doi]
- Representing reductions of NP-complete problems in logical frameworks: a case studyCarsten Schürmann, Jatin Shah. [doi]
- A modal foundation for meta-variablesAleksandar Nanevski, Brigitte Pientka, Frank Pfenning. [doi]
- Mechanising Hankin and Barendregt using the Gordon-Melham axiomsMichael Norrish. [doi]
- A unified category theoretic approach to variable bindingJohn Power. [doi]
- Compiler implementation in a formal logical frameworkJason Hickey, Aleksey Nogin, Adam Granicz. [doi]
- A definitional approach to primitivexs recursion over higher order abstract syntaxS. J. Ambler, Roy L. Crole, Alberto Momigliano. [doi]
- A formalization of an Ordered Logical Framework in Hybrid with applications to continuation machinesAlberto Momigliano, Jeff Polakow. [doi]