<p>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:</p>

<p>A linear loop is a very simple program of the form:</p>

<blockquote>
  <p><span class="math-container">$x=s$</span></p>
  
  <p>While <span class="math-container">$x\notin F$</span></p>
  
  <p><span class="math-container">$x\leftarrow Ax$</span></p>
</blockquote>

<p>Where <span class="math-container">$s,x\in \mathbb Q^d$</span> and <span class="math-container">$A\in \mathbb Q^{d\times d}$</span> is a matrix. The set <span class="math-container">$F$</span> is a terminating condition, which can be some simply described set (e.g., a polytope, or a semialgebraic set).</p>

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

<p>You can have a look at the paper <a href="https://arxiv.org/abs/1303.2981" rel="noreferrer">On the Complexity of the Orbit Problem</a> as a good starting point.</p>

CC BY-SA 4.0
2019-05-17T10:09:04.480Z
2019-05-17T10:09:04.480Z
Shaull
<p>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. </p>

<ul>
<li><p>Thierry Coquand, Henri Lombardi. <a href="http://www.cse.chalmers.se/~coquand/FISCHBACHAU/AlgebraLogicCoqLom.pdf" rel="noreferrer"><em>A logical approach to abstract algebra</em></a>. </p>

<p>This paper made a <strong>huge</strong> 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. </p></li>
<li><p>Henri Lombardi and Claude Quitté have a (freely-available) textbook, <a href="https://arxiv.org/pdf/1605.04832" rel="noreferrer"><em>Commutative algebra: Constructive methods</em></a>. </p>

<p>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.</p></li>
</ul>

<p>There are also a number of very interesting PhD theses in the area:</p>

<ul>
<li><p>Andres Mörtberg's PhD thesis <a href="http://www.cs.cmu.edu/~amoertbe/thesis/thesis.pdf" rel="noreferrer"><em>Formalizing Refinements and Constructive Algebra
in Type Theory</em></a> </p>

<p>Once you have a constructive proof, you've got an an algorithm. This thesis looks at making those algorithms efficient. </p></li>
<li><p>Bassel Mannaa's PhD thesis, <a href="https://gupea.ub.gu.se/bitstream/2077/48250/1/gupea_2077_48250_1.pdf" rel="noreferrer"><em>Sheaf Semantics in Constructive Algebra and Type Theory</em></a></p>

<p>In this thesis, he proves the correctness of the Newton-Puiseux theorem constructively, <em>as well as</em> the independence of Markov's principle. It offers a nice example of how sheaf-semantic methods have applications in both geometry and logic.</p></li>
<li><p>Ingo Blechschmidt's PhD thesis, <a href="http://rawgit.com/iblech/internal-methods/master/notes.pdf" rel="noreferrer"><em>Using the internal language of toposes in algebraic geometry,</em></a></p>

<p>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. </p></li>
</ul>

<p>It's also worth pointing out the following reference:</p>

<ul>
<li><p>Saunders Mac Lane, Ieke Moerdijk. <a href="https://link.springer.com/book/10.1007/978-1-4612-0927-0" rel="noreferrer"><em>Sheaves in Geometry and Logic Sheaves in Geometry and Logic: A first introduction to topos theory</em></a>. </p>

<p>A lot of the technology used in this work comes via the connections between topos theory, logic and geometry. This is the standard reference, though I mostly learned it via the papers of Steve Vickers instead. </p></li>
</ul>

CC BY-SA 4.0
2019-05-21T09:31:08.920Z
2019-05-21T09:31:08.920Z
Neel Krishnaswami
<p>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.</p>

<p>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?</p>

CC BY-SA 4.0
2019-05-16T20:43:10.847Z
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.
Henning Basold
CC BY-SA 4.0
2019-05-21T12:38:36.737Z
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.
Syed Muhammad Asad
CC BY-SA 4.0
2019-05-21T21:04:30.587Z
@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
<pl.programming-languages><type-theory><algebra>
Applications of algebraic geometry in type theory/programming language theory
xrq
# Applications of algebraic geometry in type theory/programming language theory

(Asked by: username_0 on 2019-05-16)

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?

**Tags:** pl.programming-languages, type-theory, algebra

> **Comments:**
> **username_1**: 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.  
> **username_2**: 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.  
> **username_0**: @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.  

---

## 2 answers

### Answer by username_4 on 2019-05-21. Score: 15 | Accepted answer

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*](http://www.cse.chalmers.se/~coquand/FISCHBACHAU/AlgebraLogicCoqLom.pdf).

  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*](https://arxiv.org/pdf/1605.04832).

  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*](http://www.cs.cmu.edu/~amoertbe/thesis/thesis.pdf)

  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*](https://gupea.ub.gu.se/bitstream/2077/48250/1/gupea_2077_48250_1.pdf)

  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,*](http://rawgit.com/iblech/internal-methods/master/notes.pdf)

  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:

* Saunders Mac Lane, Ieke Moerdijk. [*Sheaves in Geometry and Logic Sheaves in Geometry and Logic: A first introduction to topos theory*](https://link.springer.com/book/10.1007/978-1-4612-0927-0).

  A lot of the technology used in this work comes via the connections between topos theory, logic and geometry. This is the standard reference, though I mostly learned it via the papers of Steve Vickers instead.


---

### Answer by username_3 on 2019-05-17. Score: 8

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](https://arxiv.org/abs/1303.2981) as a good starting point.


---

