diff --git a/topics/exercises/README.txt b/topics/exercises/README.txt
index 9ddf22a7..947058ff 100644
--- a/topics/exercises/README.txt
+++ b/topics/exercises/README.txt
@@ -2,6 +2,7 @@ while1	- a DCG parser for a fragment of While
 while2	- a DCG parser for While
 while3	- big step semantics for While (+ a DCG parser)
 while4	- small step semantics for While (+ a DCG parser)
+while5  - typed While
 xml1	- a DCG parser for XML subset (elements only)
 xml2	- a DCG parser for XML subset (elements and attributes)
 nb1	- abstract syntax for NB
diff --git a/topics/exercises/while5/Makefile b/topics/exercises/while5/Makefile
new file mode 100644
index 00000000..fe7165e7
--- /dev/null
+++ b/topics/exercises/while5/Makefile
@@ -0,0 +1,9 @@
+test:
+	swipl -f RunTypeChecker.pro -t "main('input.txt')"
+
+debug:
+	cat input.txt
+	swipl -s RunTypeChecker.pro
+
+clean:
+	rm -rf *~
diff --git a/topics/exercises/while5/Parser.pro b/topics/exercises/while5/Parser.pro
new file mode 100644
index 00000000..cd732b02
--- /dev/null
+++ b/topics/exercises/while5/Parser.pro
@@ -0,0 +1,147 @@
+%% Parser for While language
+% Program is a list of statements
+program(S) --> statements(S).
+
+% Non-empty list
+statements(slist(H,T)) -->
+ statement(H),
+ keyword(";"),
+ statements(T).
+
+% Empty list
+statements(S) --> statement(S).
+
+%% Statements
+% Variable declaration
+statement(decl(V)) -->
+ keyword("var"),
+ identifier(V).
+
+% Skip statement
+statement(skip) -->
+ keyword("skip").
+
+% Assign statement
+statement(assign(identifier(V),E)) -->
+ identifier(V),
+ keyword(":="),
+ aexpression(E).
+
+% Conditional statement
+statement(ifthenelse(E,S1,S2)) -->
+ keyword("if"),
+ bexpression(E),
+ keyword("then"),
+ statement(S1),
+ keyword("else"),
+ statement(S2).
+
+% Loop statement
+statement(while(E,S)) -->
+ keyword("while"),
+ bexpression(E),
+ keyword("do"),
+ statement(S).
+
+
+%% Arithmetic expressions
+% Number is a an arithmetic expression
+aexpression(number(N)) --> number(N).
+
+% Variable reference is a an arithmetic expression
+aexpression(identifier(V)) --> identifier(V).
+
+% A sum of arithmetic expressions is also an arithmetic expression
+aexpression(add(E1,E2)) -->
+ keyword("("),
+ aexpression(E1),
+ keyword("+"),
+ aexpression(E2),
+ keyword(")").
+
+% Same with subtraction
+aexpression(sub(E1,E2)) -->
+ keyword("("),
+ aexpression(E1),
+ keyword("-"),
+ aexpression(E2),
+ keyword(")").
+
+% ...and multiplication
+aexpression(mul(E1,E2)) -->
+ keyword("("),
+ aexpression(E1),
+ keyword("*"),
+ aexpression(E2),
+ keyword(")").
+
+
+%% Boolean expressions
+% Boolean primitives are boolean expressions
+bexpression(true) --> keyword("true").
+bexpression(false) --> keyword("false").
+
+% Comparison is a boolean expression: equality
+bexpression(equals(E1,E2)) -->
+ aexpression(E1),
+ keyword("="),
+ aexpression(E2).
+
+% Comparison is a boolean expression: less than or equal to
+bexpression(lte(E1,E2)) -->
+ aexpression(E1),
+ keyword("≤"),
+ aexpression(E2).
+
+% Negation is a boolean expression
+bexpression(not(E)) -->
+ keyword("¬"),
+ bexpression(E).
+
+% Disjunction of boolean expressions is also a boolean expression
+bexpression(and(E1,E2)) -->
+ keyword("("),
+ bexpression(E1),
+ keyword("^"),
+ bexpression(E2),
+ keyword(")").
+
+
+%% Low-level details
+% Dealing with layout
+layout --> [0' ], layout.  %'  space
+layout --> [0'	], layout. %'  tab
+layout --> [10], layout.   %   newline
+layout --> [].
+
+% Keywords are space-consuming strings
+keyword(X) -->
+ layout,
+ string(X).
+
+% Bare strings
+string([],X,X).
+string([H|T1],[H|T2],X) :- string(T1,T2,X).
+
+% Numbers are space-consuming digits
+number(N) -->
+ layout,
+ digit(H), digits(T),
+ { number_chars(N,[H|T]) }.
+
+% Bare digits
+digits([H|T]) --> digit(H), digits(T).
+digits([]) --> [].
+digit(H,[H|T],T) :- H >= 0'0, H =< 0'9.
+
+% Identifiers are space-consuming letters
+identifier(V) -->
+ layout,
+ letter(H), letters(T),
+ { atom_chars(V,[H|T]) }.
+
+% Bare letters
+letters([H|T]) --> letter(H), letters(T).
+letters([]) --> [].
+letter(H,[H|T],T) :- H >= 0'a, H =< 0'z.
+
diff --git a/topics/exercises/while5/RunTypeChecker.pro b/topics/exercises/while5/RunTypeChecker.pro
new file mode 100644
index 00000000..8488fb90
--- /dev/null
+++ b/topics/exercises/while5/RunTypeChecker.pro
@@ -0,0 +1,20 @@
+:- ['Parser.pro','mappings.pro','compExpr.pro','smallStm.pro','Types.pro'].
+
+main(File) :-
+ parseFile(File,program,S),
+ write(S),nl,nl,
+ type(S,[],M,T),
+ %execute(S,[],M),
+ write(M),nl.
+
+parseFile(File,P,R) :-
+ open(File,read,Stream,[]), 
+ read_stream_to_codes(Stream, Contents),
+ close(Stream),
+ apply(P,[R,Contents,Rest]),
+ eof(Rest,_).
+
+eof([],[]).
+eof([0' |T],R) :- eof(T,R). %'
+eof([10|T],R) :- eof(T,R).
+
diff --git a/topics/exercises/while5/Types.pro b/topics/exercises/while5/Types.pro
new file mode 100644
index 00000000..d4ca645a
--- /dev/null
+++ b/topics/exercises/while5/Types.pro
@@ -0,0 +1,39 @@
+:- ['Parser.pro'].
+
+% type(Expression,DeclaredIn,DeclaredOut,Type), where Type = unit
+% type(Expression,Declared,Type), where Type = bool or nat
+
+%% StateDents have the 'unit' type
+type(slist(S1,S2),D1,D2,unit) :-
+ type(S1,D1,D3,unit),
+ type(S2,D3,D2,unit).
+
+type(skip,D,D,unit).
+type(decl(X),D1,D2,unit) :- declare(D1,X,D2).
+type(assign(identifier(X),E),D,D,unit) :-
+ type(E,D,nat),
+ isdeclared(D,X).
+type(ifthenelse(E,S1,S2),D1,D2,unit) :-
+ type(E,D1,bool),
+ % we assume no local variable declarations
+ type(S1,D1,D2,unit),
+ type(S2,D1,D2,unit).
+
+type(while(E,S),D1,D2,unit) :-
+ type(E,D1,bool),
+ type(S,D1,D2,unit).
+
+%% Arithmetic expressions have the 'nat' type
+type(number(N),_,nat).
+type(identifier(N),D,nat) :- isdeclared(D,N).
+type(add(E1,E2),D,nat) :- type(E1,D,nat), type(E2,D,nat).
+type(sub(E1,E2),D,nat) :- type(E1,D,nat), type(E2,D,nat).
+type(Dul(E1,E2),D,nat) :- type(E1,D,nat), type(E2,D,nat).
+
+%% Boolean expressions have the 'bool' type
+type(true,_,bool).
+type(false,_,bool).
+type(equals(E1,E2),D,bool) :- type(E1,D,nat), type(E2,D,nat).
+type(lte(E1,E2),D,bool) :- type(E1,D,nat), type(E2,D,nat).
+type(not(E),D,bool) :- type(E,D,bool).
+type(and(E1,E2),D,bool) :- type(E1,D,bool), type(E2,D,bool).
diff --git a/topics/exercises/while5/compExpr.pro b/topics/exercises/while5/compExpr.pro
new file mode 100644
index 00000000..6a3d30de
--- /dev/null
+++ b/topics/exercises/while5/compExpr.pro
@@ -0,0 +1,121 @@
+%% Small-step transition relation for expressions
+/*
+% Closure for arithmetic expressions
+evala(A,M,V) :-
+ evalastep(A,M,V),
+ number(V).
+
+evala(A1,M,V) :-
+ evalastep(A1,M,A2),
+ evala(A2,M,V).
+
+% Closure for boolean expressions
+evalb(B,M,V) :-
+ evalbstep(B,M,V),
+ isbool(V).
+
+evalb(B1,M,V) :-
+ evalbstep(B1,M,B2),
+ evalb(B2,M,V).
+*/
+
+%% Evaluate arithmetic expressions
+% Number is evaluated to its value
+evalastep(number(V),_,V).
+
+% Variable reference is evaluated to its current value
+evalastep(identifier(X),M,number(Y)) :- lookup(M,X,Y).
+
+%% Adddition
+% Case 1: add number to number
+evalastep(add(number(V1),number(V2)),_,number(V)) :- V is V1 + V2.
+% Case 2: add number to expression
+evalastep(add(number(V1),A2),M,add(number(V1),A3)) :- evalastep(A2,M,A3).
+% Case 3: add expression to something
+evalastep(add(A1,A2),M,add(A3,A2)) :- evalastep(A1,M,A3).
+
+%% Subtraction
+% Case 1: subtract number from number
+evalastep(sub(number(V1),number(V2)),_,number(V)) :- V is V1 - V2.
+% Case 2: subtract number from expression
+evalastep(sub(number(V1),A2),M,sub(number(V1),A3)) :- evalastep(A2,M,A3).
+% Case 3: subtract expression from something
+evalastep(sub(A1,A2),M,sub(A3,A2)) :- evalastep(A1,M,A3).
+
+%% Multiplication
+% Case 1: number times number
+evalastep(mul(number(V1),number(V2)),_,number(V)) :- V is V1 * V2.
+% Case 2: number times expression
+evalastep(mul(number(V1),A2),M,sub(number(V1),A3)) :- evalastep(A2,M,A3).
+% Case 3: expression times something
+evalastep(mul(A1,A2),M,sub(A3,A2)) :- evalastep(A1,M,A3).
+
+%% Evaluate Boolean expressions
+% True is tt
+evalbstep(true,_,tt).
+
+% False is ff
+evalbstep(false,_,ff).
+
+%% Negation
+% One small step is enough
+evalbstep(not(B),M,V) :-
+ evalbstep(B,M,V1),
+ isbool(V1),
+ not(V1,V).
+% One small step is not enough
+evalbstep(not(B1),M,not(B2)) :-
+ evalbstep(B1,M,B2).
+
+%% Conjunction
+% Case 1: atomic boolean and atomic boolean
+evalbstep(and(B1,B2),_,V) :-
+ isbool(B1),
+ isbool(B2),
+ and(B1,B2,V).
+% Case 2: atomic boolean and non-atomic boolean
+evalbstep(and(B1,B2),M,and(B1,B3)) :-
+ isbool(B1),
+ evalbstep(B2,M,B3).
+% Case 3: non-atomic boolean and something
+evalbstep(and(B1,B2),M,and(B3,B2)) :-
+ evalbstep(B1,M,B3).
+
+%% Test for equality
+% Case 1: compare number with number
+evalbstep(equals(V1,V2),_,V) :-
+ number(V1),
+ number(V2),
+ equals(V1,V2,V).
+% Case 2: compare number with expression
+evalbstep(equals(V1,A2),M,equals(V1,A3)) :- 
+ number(V1),
+ evalastep(A2,M,A3).
+% Case 3: compare expression with something
+evalbstep(equals(A1,A2),M,equals(A3,A2)) :- evalastep(A1,M,A3).
+
+% Test for being less than or equal
+% Case 1: compare number with number
+evalbstep(lte(V1,V2),_,V) :-
+ number(V1),
+ number(V2),
+ lte(V1,V2,V).
+% Case 2: compare number with expression
+evalbstep(lte(V1,A2),M,lte(V1,A3)) :- 
+ number(V1),
+ evalastep(A2,M,A3).
+% Case 3: compare expression with something
+evalbstep(lte(A1,A2),M,lte(A3,A2)) :- evalastep(A1,M,A3).
+
+%% Basic operations
+equals(V1,V2,tt) :- V1 == V2.
+equals(V1,V2,ff) :- \+ V1 == V2.
+lte(V1,V2,tt) :- V1 =< V2.
+lte(V1,V2,ff) :- \+ V1 =< V2.
+not(tt,ff).
+not(ff,tt).
+and(tt,tt,tt).
+and(ff,_,ff).
+and(_,ff,ff).
+isbool(tt).
+isbool(ff).
diff --git a/topics/exercises/while5/input.txt b/topics/exercises/while5/input.txt
new file mode 100644
index 00000000..9b756eaf
--- /dev/null
+++ b/topics/exercises/while5/input.txt
@@ -0,0 +1,11 @@
+var x;
+var y;
+var z;
+y:=2;
+x:=(y+4);
+if (y = 2 ^ x = 6)
+ then
+  z := y
+ else
+  z := 1000;
+while x≤10 do x := (x + 1)
diff --git a/topics/exercises/while5/mappings.pro b/topics/exercises/while5/mappings.pro
new file mode 100644
index 00000000..bd22896a
--- /dev/null
+++ b/topics/exercises/while5/mappings.pro
@@ -0,0 +1,17 @@
+% Function lookup for functions represented as lists of pairs
+lookup(M,X,Y) :- append(_,[(X,Y)|_],M).
+isdeclared(D,X) :- member(X,D).
+
+% Fresh variables can be declared
+declare([],X,[X]).
+declare([H|T1],X,[H|T2]) :-
+ \+ H = X,
+ declare(T1,X,T2).
+
+% Variable values can be updated
+update([(X,_)|M],X,Y,[(X,Y)|M]).
+update([(X1,Y1)|M1],X2,Y2,[(X1,Y1)|M2]) :-
+ \+ X1 = X2,
+ update(M1,X2,Y2,M2).
+
+
diff --git a/topics/exercises/while5/smallStm.pro b/topics/exercises/while5/smallStm.pro
new file mode 100644
index 00000000..01684101
--- /dev/null
+++ b/topics/exercises/while5/smallStm.pro
@@ -0,0 +1,44 @@
+%% Small-step transition relation for statement execution
+execute(S,M1,M2) :-
+ executionstep(S,M1,M2).
+
+execute(S1,M1,M3) :-
+ executionstep(S1,M1,S2,M2),
+ execute(S2,M2,M3).
+
+% Skip statement
+executionstep(skip,M,M).
+
+% Variable declaration
+executionstep(decl(V),M1,M2) :-
+ \+ lookup(M1,V,_),
+ update(M1,V,M2).
+
+%% Sequential composition
+% Only a small step for S1
+executionstep(slist(S1,S2),M1,slist(S1p,S2),M2) :-
+ executionstep(S1,M1,S1p,M2).
+% Done with S1, only S2 is left now
+executionstep(slist(S1,S2),M1,S2,M2) :-
+ executionstep(S1,M1,M2).
+ 
+%% Assignment
+% Right hand side is a number
+executionstep(assign(identifier(X),N),M1,M2) :-
+ number(N),
+ update(M1,X,N,M2).
+% Right hand side evaluation progresses
+executionstep(assign(identifier(X),A1),M,assign(identifier(X),A2),M) :-
+ evalastep(A1,M,A2).
+
+%% Conditional statement
+% True condition
+executionstep(ifthenelse(tt,S1,_),M,S1,M).
+% False condition
+executionstep(ifthenelse(ff,_,S2),M,S2,M).
+% Non-atomic condition
+executionstep(ifthenelse(B1,S1,S2),M,ifthenelse(B2,S1,S2),M) :-
+ evalbstep(B1,M,B2).
+
+% Loop statement
+executionstep(while(B,S),M,ifthenelse(B,slist(S,while(B,S)),skip),M).