Geometric Interpretation of Computation Being from Physics, I have been trained to look into a lot of problems from a geometrical point of view. For example the differential geometry of manifolds in dynamical systems etc. When I read the foundations of computer science, I always try to find geometric interpretations. Like a plausible geometric interpretation of recursively enumerable sets (I worked on a part where I tried to connect them with Algebraic Geometry by exploiting equivalence with Diophantine Sets but the connection seemed forced and I could not find a "natural" expression of the facts in that formulation) or a beautiful geometric result for a simple algorithm for sorting numbers. Though I am not an expert I have read surveys on Geometric Complexity Theory and it is surely an interesting program but I am more interested in having a geometric view of extremely fundamental concepts like the dynamics of a Turing Machine, Lambda Calculus or the structure of (un)computable sets (rather than specific problems). Is it a hopeless job to find geometrical structure in these objects or can one expect some intricate results? Is there any formulation of TCS which treats it geometrically?
The semantics of computer programs can be understood geometrically in three distinct (and apparently incompatible) ways. 


The oldest approach is via domain theory. The intuition behind domain theory arises from the asymmetry behind termination and nontermination. 

When treating programs extensionally (ie, only looking at their I/O behavior, and not their internal structure), it is always possible to confirm in finite time that a program halts -- you just wait until it stops. However, it's not possible to confirm that a program doesn't halt, because no matter how long you wait, there is always a halting program that will run for a few more steps than you waited. 

As a result, halting and looping can be viewed as forming a topological space (the  Sierpiński space). This lifts to richer notions of observation (via the Scott topology), and you can thereby interpret programs as elements of  topological spaces. These spaces are generally quite surprising from a traditional point of view -- domains are generally not Hausdorff.   

The best topological introduction I know to these ideas is Steve Vickers' short and extremely accessible Topology via Logic. It can be understood as a sort of warm-up for Peter Johnstone's significantly more formidable Stone Spaces.  

If you are looking for online lecture notes, let me suggest Martin Escardo's Synthetic Topology of Data Types and Classical Spaces. 
Another view arises from concurrency theory. A concurrent program can be understood as having multiple valid executions (sequences of states), depending on how races are resolved. Then, the set of executions can be viewed as a space, with each possible sequence of states understood as a path through this space. Then, methods from algebraic topology and homotopy theory can be applied to derive invariants about the program execution. 

Nir Shavit and Maurice Herlihy uses this idea to prove the impossibility of certain distributed algorithms, for which they won the 2004 G&ouml;del prize. (See The Topological Structure of Asynchronous Computation.) Eric Goubault has a survey paper explaining the relevant ideas in Some Geometric Perspectives in Concurrency Theory.  
Most recently, it has been observed that the structure of the identity type in dependent type theory corresponds very closely with the notion of homotopy type in homotopy theory -- so closely, in fact, that dependent type theory can actually be seen as a sort of "synthetic homotopty theory"! (Vladimir Voevodsky has joked that he spent several years developing a new calculus for homotopy theory, only to discover that his colleagues in the CS department were already teaching it to undergraduates.)

See cody's link above to the homotopy type theory book.


Interestingly, these three views seem incompatible with each other, or at least very difficult to reconcile. Dependent type theory is a total language, so nontermination (and the Scott topology) does not arise in it. It is also confluent, so the view of computations-as-spaces doesn't arise either. Similarly, formulating concurrency in terms of domain theory has proved ferociously difficult, and a completely satisfactory account is still an open problem.