Abstract. We illustrate a methodology for formalizing and reasoning about Abadi and Cardelli’s object-based calculi, in (co)inductive type theory, such as the Calculus of (Co)Ind...
Alberto Ciaffaglione, Luigi Liquori, Marino Micula...
Abstract. Higher-order abstract syntax (HOAS) refers to the technique of representing variables of an object-language using variables of a meta-language. The standard first-order a...
We give a short description of Hybrid, a new tool for interactive theorem proving, s introduced in [4]. It provides a form of Higher Order Abstract Syntax (HOAS) combined consiste...