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?
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.