Strongly typed term representations in Coq

Nick Benton, Chung-Kil Hur, Andrew Kennedy, Conor McBride

Research output: Contribution to journalArticle

26 Citations (Scopus)

Abstract

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 heterogeneous equality.
Original languageEnglish
Pages (from-to)141-159
Number of pages19
JournalJournal of Automated Reasoning
Volume49
Issue number2
DOIs
Publication statusPublished - Aug 2012

Fingerprint

Substitution reactions
Strapping
Syntactics
Computer programming languages

Keywords

  • Coq proof assistant
  • typed object languages
  • de Bruijn indices

Cite this

Benton, Nick ; Hur, Chung-Kil ; Kennedy, Andrew ; McBride, Conor. / Strongly typed term representations in Coq. In: Journal of Automated Reasoning. 2012 ; Vol. 49, No. 2. pp. 141-159.
@article{c90412a303e6498f904ec03e71786675,
title = "Strongly typed term representations in Coq",
abstract = "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 heterogeneous equality.",
keywords = "Coq proof assistant, typed object languages , de Bruijn indices",
author = "Nick Benton and Chung-Kil Hur and Andrew Kennedy and Conor McBride",
year = "2012",
month = "8",
doi = "10.1007/s10817-011-9219-0",
language = "English",
volume = "49",
pages = "141--159",
journal = "Journal of Automated Reasoning",
issn = "0168-7433",
number = "2",

}

Strongly typed term representations in Coq. / Benton, Nick; Hur, Chung-Kil; Kennedy, Andrew; McBride, Conor.

In: Journal of Automated Reasoning, Vol. 49, No. 2, 08.2012, p. 141-159.

Research output: Contribution to journalArticle

TY - JOUR

T1 - Strongly typed term representations in Coq

AU - Benton, Nick

AU - Hur, Chung-Kil

AU - Kennedy, Andrew

AU - McBride, Conor

PY - 2012/8

Y1 - 2012/8

N2 - 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 heterogeneous equality.

AB - 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 heterogeneous equality.

KW - Coq proof assistant

KW - typed object languages

KW - de Bruijn indices

U2 - 10.1007/s10817-011-9219-0

DO - 10.1007/s10817-011-9219-0

M3 - Article

VL - 49

SP - 141

EP - 159

JO - Journal of Automated Reasoning

JF - Journal of Automated Reasoning

SN - 0168-7433

IS - 2

ER -