# Applications of algebraic geometry in type theory/programming language theory

Lately, I have become interested in algebraic geometry and have started reading on it. I still know very little about this field, but I do want to know if it has any connection with my main field, type theory and programming languages.

I know that algebraic topology has a lot of applications in type theory (homotopy type theory, and many more), but what about algebraic geometry, besides that both type theory/PL theory and AG are good motivators of category theory?

• This is not an answer to your question, but algebraic topology is also applied in concurrency theory. Have a look at Directed homotopy and there is a paper at Fossacs 2019 about that as well. Commented May 16, 2019 at 20:43
• Me too interested in Computer programming and mathematics research student. My supervisor is topologist. But I want to do research in mathematics related to computer science like linear algebra. I need help in order to search my thesis topic so that I can made research in theoretical computer science but I don't know from where I should start. Need help for my thesis topic so that I can made research in my interested field. Commented May 21, 2019 at 12:38
• @SyedMuhammadAsad I am also a student so I'm not the person to ask. You should consult some experts in this field. Topology (particularly algebraic) has deep connections to type theory so you may start there.
– xrq
Commented May 21, 2019 at 21:04

To my knowledge (which is definitely incomplete), there has been relatively little work on this, presumably because it requires assimilating two relatively intricate bodies of knowledge. However, little does not mean nonexistent. Thierry Coquand and his collaborators have written quite a few papers on the connections between commutative algebra and constructive logic.

• Thierry Coquand, Henri Lombardi. A logical approach to abstract algebra.

This paper made a huge impression on me as a grad student -- the confident and free way that it used ideas from proof theory and model theory to do nontrivial, proper mathematics is one I greatly admired, and to which I still aspire.

• Henri Lombardi and Claude Quitté have a (freely-available) textbook, Commutative algebra: Constructive methods.

As the title suggests, this is commutative algebra rather than algebraic geometry, but since commutative algebra provides much of the infrastructure for algebraic geometry this will still be of interest.

There are also a number of very interesting PhD theses in the area:

• Andres Mörtberg's PhD thesis Formalizing Refinements and Constructive Algebra in Type Theory

Once you have a constructive proof, you've got an an algorithm. This thesis looks at making those algorithms efficient.

• Bassel Mannaa's PhD thesis, Sheaf Semantics in Constructive Algebra and Type Theory

In this thesis, he proves the correctness of the Newton-Puiseux theorem constructively, as well as the independence of Markov's principle. It offers a nice example of how sheaf-semantic methods have applications in both geometry and logic.

• Ingo Blechschmidt's PhD thesis, Using the internal language of toposes in algebraic geometry,

This thesis looks at redoing many of the usual proofs of algebraic geometry in the internal language of the little Zariski topos associated with a scheme, yielding a kind of "synthetic algebraic geometry". (He also does "synthetic scheme theory" using the big Zariski topos). As you would expect, since topoi are not generally Boolean, the proofs have to be done in an intuitionistic style.

It's also worth pointing out the following reference:

This might not be exactly what you're looking for, but one application of algebraic geometry in programming languages is the analysis of linear loops:

A linear loop is a very simple program of the form:

$$x=s$$

While $$x\notin F$$

$$x\leftarrow Ax$$

Where $$s,x\in \mathbb Q^d$$ and $$A\in \mathbb Q^{d\times d}$$ is a matrix. The set $$F$$ is a terminating condition, which can be some simply described set (e.g., a polytope, or a semialgebraic set).

The analysis of these loops often amounts to analyzing the orbit of the matrix $$A$$, namely $$\{A^ns: n\in \mathbb N\}$$. This, in turn, involves the analysis of powers of the eigenvalues of $$A$$, whose behaviour has close connection to concepts in algebraic geometry (e.g. Masser's basis theorem).

You can have a look at the paper On the Complexity of the Orbit Problem as a good starting point.