The Turing Machine
The Turing Machine was first proposed by Alan Turing in 1936 as the first rigorously definied model of computation. It is essentially the foundation of modern computers and can do everything that a real computer can do. It was not ever intended for construction, but is more of a thought experiment.
A Turing Machine (TM) has an infinite tape (memory), with a tape head that can read, write and move around on the tape. There is also a finite-state program comprised of a table of instructions which controls the tape head.
Context-Free Grammars
Context-Free Languages (CFLs) are more powerful than Regular Languages (provably so) and can be defined by means of Context-Free Grammars or Push-Down Automata. Any context free language can be represented with either of these methods. CFLs closely relate to both human languages and programming languages and their applications tend to fall within these fields.
A Context-Free Grammar (CFG) is essentially a collection of substitution rules of the form 
Push-Down Automata
Push-Down Automata (PDAs) are an example of a Context-Free Language, they make use of a stack containing data and have to power to make transitions based on the top of the stack, and also manipulate the stack by popping and pushing new values. They are essentially an implementation of NFA's with an additional stack.
Put together: Given an input signal, current state, and stack symbol, the automaton can follow a transition to another state, and optionally manipulate (push or pop) the stack.
Rules of Inference
Proof Theory allows the representation of mathematical proofs facilitates the analysis of proofs by expressing them syntactically. For example, in the sequent below the formulas 
We can form a collection of proof rules which allow us to infer new forumlae from existing ones. These inference rules are a relation between premise formulae and conclusions. Such rules take the general form:
