{"size": 1615, "ext": "scrbl", "max_stars_repo_path": "cur-paper/abstract.scrbl", "max_stars_repo_name": "bluephoenix47/cic-redex", "max_stars_repo_stars_event_min_datetime": "2015-07-23T20:56:11.000Z", "max_stars_repo_stars_event_max_datetime": "2022-01-07T04:34:29.000Z", "max_issues_repo_path": "cur-paper/abstract.scrbl", "max_issues_repo_name": "bluephoenix47/cic-redex", "max_issues_repo_issues_event_min_datetime": "2015-09-09T22:57:20.000Z", "max_issues_repo_issues_event_max_datetime": "2021-04-19T20:55:34.000Z", "max_forks_repo_path": "cur-paper/abstract.scrbl", "max_forks_repo_name": "dmelcer9/cur", "max_forks_repo_forks_event_min_datetime": "2015-09-17T17:13:27.000Z", "max_forks_repo_forks_event_max_datetime": "2021-08-14T01:17:46.000Z"}
{"max_stars_count": 215, "max_issues_count": 125, "max_forks_count": 17, "avg_line_length": 53.8333333333, "max_line_length": 80, "alphanum_fraction": 0.8185758514}
#lang scribble/base
@(require
  scribble/manual
  "defs.rkt")

Theoreticians often use sophisticated notation to communicate and reason about
key ideas in their theories and models.
Notation is often domain-specific or even invented on-the-fly when creating a
new theory or model.
Proof assistants aid theoreticians by rigorously checking formal models, but
have poor support for allowing users to @emph{conveniently} define and use
@emph{sophisticated} notation.
For example, in a proof assistant like Coq or Agda, users can easily define
simple notation like @code{Γ ⊢ e : t}, but to use BNF notation the user must use
a preprocessing tool external to the proof assistant, which is cumbersome.

To support convenient and sophisticated extension, we can use @emph{language
extension} as a fundamental part of the design of a proof assistant.
By starting from language extension we can not only facilitate convenient and
sophisticated user-defined extensions, but also get a single, compositional
system for writing all extensions to the core proof language.

We describe how to design a language-extension system that supports safe,
convenient, and sophisticated user-defined extensions, and how to design a
proof assistant based on language extension.
We evaluate this design by building a proof assistant that features a small
dependent type theory as the core language and implementing the following
extensions in small user-defined libraries: pattern matching for inductive
types, dependently typed staged meta-programming, a tactic language, and BNF
and inference-rule notation for inductive type definitions.