Skip to content

Abstracts.2020.PLGrammars

Jump to bottom
Fabian edited this page May 25, 2021 · 1 revision

Modeling Programming Languages in Grammatical Framework

by Warrick Macmillan

Abstract

In this talk I will discuss how to use Grammatical Framework (GF) to model the syntax of a programming language.

GF is a strongly-typed domain-specific language and logical framework for specifying abstract and concrete syntax. Once an abstract syntax has been specified, one can view a corresponding concrete syntax as a model. The parsing and linearization pipeline in GF gives it translation capabilities for both controlled natural languages and programming languages (PLs), and therefore allows one hypothetically to translate between, for instance, a mathematics text and code running in an interactive theorem prover.

The talk will be structured as follows:

  1. Introduce GF
  2. Discuss what it means to model a PL in GF
  3. Go through some increasingly sophisticated case studies of
    • a simple language for arithmetic,
    • a simply-typed lambda calculus with natural numbers, also known as Gödel’s System T, and
    • a dependently-typed lambda calculus

I will stress both the formal aspects of these programming languages and the nuance and difficulty needed to capture natural language representations that are able to be understood by non-computer scientists.

Material

  • Grammatical Framework for the working mathematician tutorial
  • Gödel’s System T in Grammatical Framework tutorial and code
Clone this wiki locally