Strongly Typed Term Representations in Coq (draft)
Nick Benton, Chung-Kil Hur, Andrew Kennedy and Conor McBride.
Submitted to Journal of Automated Reasoning: Special issue on Binding, Substitution and Naming.
There are two approaches to formalizing the syntax of typed object languages in a proof assistant or programming language. The extrinsic approach is to first define a type that encodes untyped object expressions and then make a separate definition of typing judgements over the untyped terms. The intrinsic approach is to make a single definition that captures well-typed object expressions, so ill-typed expressions cannot even be expressed. Intrinsic encodings are attractive and naturally enforce the requirement that metalanguage operations on object expressions, such as substitution, respect object types. The price is that the metalanguage types of intrinsic encodings and operations involve non-trivial dependency, adding significant complexity. This paper describes intrinsic-style formalizations of both simply-typed and polymorphic languages, and basic syntactic operations thereon, in the Coq proof assistant. The Coq types encoding object-level variables (de Bruijn indices) and terms are indexed by both type and typing environment. One key construction is the boot-strapping of definitions and lemmas about the action of substitutions in terms of similar ones for a simpler notion of renamings. In the simply-typed case, this yields definitions that are free of any use of type equality coercions. In the polymorphic case, some substitution operations do still require type coercions, which we at least partially tame by uniform use of heterogenous equality.
Coq source for simply-typed language Coq source for polymorphically-typed language
Some Domain Theory and Denotational Semantics in Coq
Nick Benton, Andrew Kennedy and Carsten Varming.
22nd International Conference on Theorem Proving in Higher Order Logics (TPHOLs'09), August 2009.
We present a Coq formalization of constructive omega-cpos (extending earlier work by Paulin-Mohring) up to and including the inverse-limit construction of solutions to mixed-variance recursive domain equations, and the existence of invariant relations on those solutions. We then define operational and denotational semantics for both a simply-typed CBV language with recursion and an untyped CBV language, and establish soundness and adequacy results in each case.
Talk on typed representation of syntax used in this work, presented at Semantics Lunch at University of Cambridge Computer Laboratory.