Book contents
- Frontmatter
- Contents
- Introduction
- Definability and elementary equivalence in the Ershov difference hierarchy
- A unified approach to algebraic set theory
- Brief introduction to unprovability
- Higher-order abstract syntax in type theory
- An introduction to b-minimality
- The sixth lecture on algorithmic randomness
- The inevitability of logical strength: Strict reverse mathematics
- Applications of logic in algebra: Examples from clone theory
- On finite imaginaries
- Strong minimal covers and a question of Yates: The story so far
- Embeddings into the Turing degrees
- Randomness—beyond Lebesgue measure
- The derived model theorem
- Forcing axioms and cardinal arithmetic
- Hrushovski's amalgamation construction
Higher-order abstract syntax in type theory
Published online by Cambridge University Press: 28 January 2010
- Frontmatter
- Contents
- Introduction
- Definability and elementary equivalence in the Ershov difference hierarchy
- A unified approach to algebraic set theory
- Brief introduction to unprovability
- Higher-order abstract syntax in type theory
- An introduction to b-minimality
- The sixth lecture on algorithmic randomness
- The inevitability of logical strength: Strict reverse mathematics
- Applications of logic in algebra: Examples from clone theory
- On finite imaginaries
- Strong minimal covers and a question of Yates: The story so far
- Embeddings into the Turing degrees
- Randomness—beyond Lebesgue measure
- The derived model theorem
- Forcing axioms and cardinal arithmetic
- Hrushovski's amalgamation construction
Summary
Abstract. We develop a general tool to formalize and reason about languages expressed using higher-order abstract syntax in a proof-tool based on type theory (Coq). A language is specified by its signature, which consists of sets of sort and operation names and typing rules. These rules prescribe the sorts and bindings of each operation. An algebra of terms is associated to a signature, using de Bruijn notation. Then a higher-order notation is built on top of the de Bruijn level, so that the user can work with meta-variables instead of de Bruijn indices. We also provide recursion and induction principles formulated directly on the higher-order syntax. This generalizes work on the Hybrid approach to higher-order syntax in Isabelle and our earlier work on a constructive extension to Hybrid formalized in Coq. In particular, a large class of theorems that must be repeated for each object language in Hybrid is done once in the present work and can be applied directly to each object language.
Introduction. We aim to use proof assistants (in our specific case Coq [9, 6]) to formally represent and reason about languages using higher-order syntax, i.e. object languages where binding operators are expressed using binding at the meta-level. This is an active and fertile field of research. Several methods contend to become the most elegant, efficient, and easy to use. The differences stem from the approach of the researchers and the characteristics of the proof tool used.
Our starting point was the work on the Hybrid tool in Isabelle/HOL by Ambler, Crole, and Momigliano [2].
- Type
- Chapter
- Information
- Logic Colloquium 2006 , pp. 65 - 90Publisher: Cambridge University PressPrint publication year: 2009
- 2
- Cited by