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?
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:
Saunders Mac Lane, Ieke Moerdijk. Sheaves in Geometry and Logic Sheaves in Geometry and Logic: A first introduction to topos theory.
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.
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.
