Here we look at some software projects and theory that relate mathematics and computation. Such as:
 The theory of computation.
 Software that models mathematics
 The mathematics of computation.
Information about computation of mathematics on this site:
 Lambda Calculus
 Combinatory Logic
 Types
 Computation using Axiom/FriCAS language
 Computation using Scala language
Computation
I tend to think of computation as some sort of machine (or person) that takes some input and uses it to produce some output. 
This is like a mathematical function in that it always generates the same output for a given input (no side effects in Haskel parlance) so an example would be a sine function which generates the ratio of the opposite and hypotenuse for a given angle.
For computer theory we need to make this very general, a Turing machine can be looked at as either:
 An acceptor  accepts a recursively enumerable set.
 A generator  computes a recursive function
 An algorithm  solves yes/no problems.
So the input/output could be anything including an infinite sequence.
Proof Assistants
More about mathematical proof on page here.
Introduction  

COQ  Some sites with introduction texts: 

Isabelle 
Semantics
This is concerned with 'meaning' of programs as opposed to their syntax.
Operational Semantics
The computations are modeled as a state with different types of command acting on that state. 
There are two flavors of this bigstep and smallstep semantics,
Bigstep
This tends to be a recursive process of combining the commands.
For instance, in a program we might put one command after another separated by a semicolon. So we can compose commands in a sequence defined like this:

Sequence 
An assignment (assign variable 'x' to value 'a') is more complicated because we need to do something inside the state, so this is like a second level:

Assign 
The 'if' statement depends on the state:

IfTrue  

IfFalse 
Smallstep
In addition to the state we hold the commands still to be executed. This allows us to model individual steps. 
iterative process
Shows how to reduce program slightly
 Abstract machine with execution state
 Reduction rules
 iterativley do reduction steps until it cant be reduced further
NP Hard