Which model of computation to simulate to prove universality?
There's a comprehensive treatment of different Turing-complete computation models and proofs of their equivalence in Martin Davis, Computability and Unsolvability. Some of the most popular systems are described, including Turing-Machines, Post problems and general recursive functions.