@inproceedings{10.1145/976571.976572,
    Abstract = {It is well known that there are problems associated with formal systems which attempt to combine higher order abstract syntax (HOAS) with principles of induction and recursion. We describe a formal system, called Bsyntax, which we have implemented in Isabelle HOL. Our contribution is to prove the existence of a combinator for primitive recursion with parameters over HOAS. The definition of the combinator is facilitated by the use of terms with infinite contexts. In particular, our work is purely definitional, and is thus consistent with classical logic and choice. An immediate payoff is that we obtain a primitive recursive definition of higher order substitution. We give a presheaf model of Bsyntax, providing additional semantic validation of Bsyntax's principles of recursion. We outline an application of our work to mechanized reasoning about the compiler intermediate language MIL-lite [2].},
    Address = {New York, NY, USA},
    Author = {Ambler, S. J. and Crole, R. L. and Momigliano, Alberto},
    BookTitle = {Proceedings of the 2003 ACM SIGPLAN Workshop on Mechanized Reasoning about Languages with Variable Binding},
    File = {A\_definitional\_approach\_to\_primitive\_rec - a - e.pdf},
    ISBN = {1581138008},
    Keywords = {Isabelle HOL, higher order abstract syntax, initial algebras, primitive recursion, topos theory, {$\lambda$}-calculus},
    Location = {Uppsala, Sweden},
    Pages = {1--11},
    Publisher = {Association for Computing Machinery},
    Series = {MERLIN '03},
    Title = {A Definitional Approach to Primitivexs Recursion over Higher Order Abstract Syntax},
    URL = {https://doi.org/10.1145/976571.976572},
    Year = {2003},
    bdsk-url-1 = {https://doi.org/10.1145/976571.976572},
    date-added = {2021-02-14 13:13:37 +0100},
    date-modified = {2021-02-14 13:13:37 +0100},
    numpages = {11},
    doi = {10.1145/976571.976572}
}

@inproceedings{10.1145/976571.976572, Abstract = {It is well known that there are problems associated with formal systems which attempt to combine higher order abstract syntax (HOAS) with principles of induction and recursion. We describe a formal system, called Bsyntax, which we have implemented in Isabelle HOL. Our contribution is to prove the existence of a combinator for primitive recursion with parameters over HOAS. The definition of the combinator is facilitated by the use of terms with infinite contexts. In particular, our work is purely definitional, and is thus consistent with classical logic and choice. An immediate payoff is that we obtain a primitive recursive definition of higher order substitution. We give a presheaf model of Bsyntax, providing additional semantic validation of Bsyntax's principles of recursion. We outline an application of our work to mechanized reasoning about the compiler intermediate language MIL-lite [2].}, Address = {New York, NY, USA}, Author = {Ambler, S. J. and Crole, R. L. and Momigliano, Alberto}, BookTitle = {Proceedings of the 2003 ACM SIGPLAN Workshop on Mechanized Reasoning about Languages with Variable Binding}, File = {A_definitional_approach_to_primitive_rec - a - e.pdf}, ISBN = {1581138008}, Keywords = {Isabelle HOL, higher order abstract syntax, initial algebras, primitive recursion, topos theory, {$\lambda$}-calculus}, Location = {Uppsala, Sweden}, Pages = {1--11}, Publisher = {Association for Computing Machinery}, Series = {MERLIN '03}, Title = {A Definitional Approach to Primitivexs Recursion over Higher Order Abstract Syntax}, URL = {https://doi.org/10.1145/976571.976572}, Year = {2003}, bdsk-url-1 = {https://doi.org/10.1145/976571.976572}, date-added = {2021-02-14 13:13:37 +0100}, date-modified = {2021-02-14 13:13:37 +0100}, numpages = {11}, doi = {10.1145/976571.976572} }