diff --git a/README.md b/README.md
index c889e02..da42d03 100644
--- a/README.md
+++ b/README.md
@@ -83,14 +83,11 @@ Like a normal programming language, you can also execute Contra programs. By def
 contra <program-name>.con
 ```
 
-This prototype also comes with a rudimentary REPL. Start a blank interactive session by typing just `contra` or load a program's functions into the REPL with `--load <program-name>.con`.
+This prototype also comes with a rudimentary REPL. Start a blank interactive session by typing just `contra`. Load files into the REPL with `:l <filename>.con` and quit with `:q`.
 
 ```shell
 # blank REPL session
 contra
-
-# load program into REPL
-contra --load <program-name>.con
 ```
 
 
diff --git a/app/Main.hs b/app/Main.hs
index 550a0c3..bec016a 100644
--- a/app/Main.hs
+++ b/app/Main.hs
@@ -9,8 +9,8 @@ import Core.Parser
   )
 import Analysis.TypeInferrer      (inferProgram)
 import Semantics.Interpreter      (runMain)
-import Semantics.REPL             (evalLoop)
-import Validation.PropertyChecker (check, redStr)
+import Semantics.REPL             (loop)
+import Validation.PropertyChecker (check)
 import Validation.Formula         (defaultRecDepth)
 
 import System.Environment (getArgs)
@@ -52,7 +52,6 @@ action ["--check",    file] = PropertyCheckDefault
 action ["--check", n, file] = PropertyCheckCustom (read n)
                               <$> (parse file >>= typecheck)
 action ["--type",     file] = TypeCheck     <$>  parse file
-action ["--load",     file] = REPL          <$> (parse file >>= typecheck)
 action ["--version"       ] = return $ Version  versionInfo
 action ["--help"          ] = return $ Fail     useInfo
 action [              file] = Execute       <$> (parse file >>= typecheck)
@@ -77,7 +76,7 @@ typecheck program =
 repl :: Program Type -> IO ()
 repl program =
   do putStrLn "✦ Contra REPL! ✦\n"
-     evalLoop program
+     loop program
 
 execute :: Program Type -> IO ()
 execute program =
@@ -105,10 +104,9 @@ useInfo =
   "How to use:\n\
        \ contra --check   <filename>.con - Check all properties in program\n\
        \ contra --check n <filename.con> - Check properties with max. recursion depth 'n'\n\
-       \ contra           <filename>.con - Execute 'main' function in program\n\
        \ contra --type    <filename>.con - Type-check and print program\n\
-  \Rudimentary REPL:\n\
-       \ contra                          - Start blank interactive REPL session\n\
-       \ contra --load    <filename>.con - Load program into REPL\n\
+       \ contra           <filename>.con - Execute 'main' function in program\n\
+       \ contra                          - Start an interactive REPL session\n\
+  \Load file into REPL with ':l <filename.con>'\n\
   \Exit REPL with ':q'"
 
diff --git a/src/Core/Syntax.hs b/src/Core/Syntax.hs
index 50d4d53..0d9b8b5 100644
--- a/src/Core/Syntax.hs
+++ b/src/Core/Syntax.hs
@@ -422,3 +422,23 @@ instance Show (Value a) where
   show (Boolean      b    _) = show b
   show (VConstructor c vs _) = c ++
     " {" ++  intercalate ", " (map show vs) ++ "}"
+
+
+-- Pretty printing in the terminal
+redStr :: String -> String
+redStr s = "\ESC[31m\STX" ++ s ++ "\ESC[m\STX"
+
+yellowStr :: String -> String
+yellowStr s = "\ESC[33m\STX" ++ s ++ "\ESC[m\STX"
+
+greenStr :: String -> String
+greenStr s = "\ESC[32m\STX" ++ s ++ "\ESC[m\STX"
+
+putStrLnRed :: String -> IO ()
+putStrLnRed = putStrLn . redStr
+
+putStrLnYellow :: String -> IO ()
+putStrLnYellow = putStrLn . yellowStr
+
+putStrLnGreen :: String -> IO ()
+putStrLnGreen = putStrLn . greenStr
diff --git a/src/Semantics/REPL.hs b/src/Semantics/REPL.hs
index 5ba6fd1..680bb8c 100644
--- a/src/Semantics/REPL.hs
+++ b/src/Semantics/REPL.hs
@@ -12,35 +12,55 @@
   This is a rudimentary REPL (Read-Eval-Print Loop) for Contra.
 
   It can be used to interact with the core language and the function definitions
-  in a program text. Load a program in the terminal using the
-  '--load <program-name>.con' option and call functions interactively.
+  in a program text. After starting the REPL, load a program in the terminal
+  with ':l <filename.con>' and start calling functions interactively.
 
 -}
 
 module Semantics.REPL where
 
 import Core.Syntax
-import Core.Parser
+import Core.Parser hiding (program)
 import Analysis.TypeInferrer
 import Semantics.PartialEvaluator
 
-import System.IO (hFlush, stdout)
+import System.IO   (hFlush, stdout)
+import System.Exit (die)
 
 
 -- Export
-evalLoop :: Program Type -> IO ()
-evalLoop p =
+loop :: Program Type -> IO ()
+loop p =
   do input <- readLine
-     if input == ":q"
-        then return ()
-        else do parsed <- parseLine input
-                typed  <- typeCheck parsed
-                let (interpreted, residual) = eval p typed
-                print interpreted
-                evalLoop residual
+     case input of
+       ":q"                -> return ()
+       (':':'l':' ': file) -> do program <- loadProgram file
+                                 putStrLn $ "Loaded file " ++ show file
+                                 loop program
+       command             -> do parsed <- parseLine command
+                                 typed  <- typeCheck parsed
+                                 let (interpreted, residual) = eval p typed
+                                 print interpreted
+                                 loop residual
 
 
 -- Utility
+loadProgram :: String -> IO (Program Type)
+loadProgram file = parse file >>= typecheck
+
+parse :: String -> IO (Program String)
+parse file =
+  do result <- parseProgram file
+     case result of
+       Left  problems -> die $ redStr $ report problems
+       Right program  -> return program
+
+typecheck :: Program String -> IO (Program Type)
+typecheck program =
+  case inferProgram program of
+    Left err -> die $ redStr err
+    Right tp -> return tp
+
 readLine :: IO String
 readLine = putStr "contra> "
            >> hFlush stdout
diff --git a/src/Validation/PropertyChecker.hs b/src/Validation/PropertyChecker.hs
index c6d5dd7..d1e6b0f 100644
--- a/src/Validation/PropertyChecker.hs
+++ b/src/Validation/PropertyChecker.hs
@@ -104,24 +104,3 @@ realise sv =
                     "Unexpected error: Property should translate to a\
                     \Boolean formula, but was a " ++ show other
 
-
--- Pretty printing
--- printCounterExample :: SMTModel -> IO ()
-
-redStr :: String -> String
-redStr s = "\ESC[31m\STX" ++ s ++ "\ESC[m\STX"
-
-yellowStr :: String -> String
-yellowStr s = "\ESC[33m\STX" ++ s ++ "\ESC[m\STX"
-
-greenStr :: String -> String
-greenStr s = "\ESC[32m\STX" ++ s ++ "\ESC[m\STX"
-
-putStrLnRed :: String -> IO ()
-putStrLnRed = putStrLn . redStr
-
-putStrLnYellow :: String -> IO ()
-putStrLnYellow = putStrLn . yellowStr
-
-putStrLnGreen :: String -> IO ()
-putStrLnGreen = putStrLn . greenStr