This is the abstract of talk that I gave in Chalmers.

Title: GF as functional-logic language

Abstract

~~~~~~

Grammatical Framework (GF) is a domain specific language for describing

natural language grammars. Despite that GF is language with very

specific application domain, it is also Turing complete and could be

used to solve nontrivial tasks in a surprising way. The design of the

language has a lot of common with other functional and logic programming

languages, most notably: Agda, Haskell, Curry and Lambda Prolog. Curry

is an interesting language which combines in a neat way the functional

and the logical paradigms but still from type theoretic point of view

this is not satisfactory because it doesn't exploit the Curry-Howard

isomorphism. Thanks to the dependent types of GF, which relates it to

Agda, and thanks to some other specifics in the type system, GF could

also be classified as functional-logic language but the two paradigms in

GF are combined in the expected way. The execution model of GF also has

a lot of common with Lambda Prolog but to cover the full semantics of GF

the virtual machine should work in two modes: narrowing and residuation.

The residuation mode is something that could be seen in the virtual

machine of Curry but not in Lambda Prolog.

In this seminar I will talk about my work in progress on a virtual

machine for running GF applications. Not everything is in place yet but

the pieces are starting to stick together. As a demo I will show how to

solve the classical n-queens problem in GF. From the logical programming

paradigm I use backtracking and from the functional paradigm I use

efficient deterministic computations. From type theoretical point of

view I define the type of all n-queens puzzles.