Commit 8742aa59 authored by Michael Kohlhase's avatar Michael Kohlhase
Browse files

more

parent f3cb9741
...@@ -58,7 +58,8 @@ from the \GF-enhanced \smglom data. ...@@ -58,7 +58,8 @@ from the \GF-enhanced \smglom data.
\GF is the ``Grammatical Framework''~\cite{Ranta:GF04,ranta-2011,GF:on}, which seems \GF is the ``Grammatical Framework''~\cite{Ranta:GF04,ranta-2011,GF:on}, which seems
uniquely suited for our purposes. It is modular, and it is based (essentially) on LF, uniquely suited for our purposes. It is modular, and it is based (essentially) on LF,
i.e. uses a dependently typed $\lambda$-calculus under the hood. i.e. uses a dependently typed $\lambda$-calculus under the hood. For our purposes,
\cite{Ranta:tlled11} is a treasure trove of insights.
\section{Using the \GF Grammatical Framework for Mathematics} \section{Using the \GF Grammatical Framework for Mathematics}
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment