diff --git a/examples/README b/examples/README
index aded98da6b2a8fe00b4436b108581c40debfa7ad..f0d448e4211714452fa12a05a57f3685ec38d860 100644
--- a/examples/README
+++ b/examples/README
@@ -40,15 +40,24 @@ But with the term:
 you will have a typing error
 
 
++ montague.acg : a file containing a very simple signature that illustrates
+(very basic) Montague semantics
 
 
++ montague-script : a file providing commands that you can run in acg.	
+You can also run it with the following command:	
+	
+	acg montague-script
+
+(press return after each command)
+
 + tag.acg : a file containing various signatures and lexicons to model
 TAG in ACG. You can run acgc on it
 
 
 
 
-+ tag-script : this file provide (commented) commands that you can run
++ tag-script : this file provides (commented) commands that you can run
 in acg. You can also run it with the following command:
 
 	acg tag-script
diff --git a/examples/montague-script b/examples/montague-script
new file mode 100644
index 0000000000000000000000000000000000000000..04153bdfd39afb776a36348e2dfa81146c2fd647
--- /dev/null
+++ b/examples/montague-script
@@ -0,0 +1,32 @@
+load d montague.acg;
+
+wait;
+
+# We first show that the term "LOVE MARY JOHN"
+# that is build in the "syntax" signature
+# is indeed of type s
+syntax analyse LOVE MARY JOHN :s ;
+
+# And, for instance, that it is not of type np
+syntax analyse LOVE MARY JOHN :np ;
+
+# How is that term realized as a string?
+# Just ask:
+syntactic_realisation analyse LOVE MARY JOHN:s;
+
+# And how is it realised semantically?
+semantics  analyse LOVE MARY JOHN:s;
+
+# Now let's check the relalisation and the meaning of
+# (EVERY MAN) (lambda x. (SOME WOMAN) (lambda y. LOVE y x)) 
+# which of course is of type s;
+syntactic_realisation semantics analyse (EVERY MAN) (lambda x. (SOME WOMAN) (lambda y. LOVE y x)) :s;
+
+# And the one of
+# (SOME WOMAN) (lambda y. (EVERY MAN) (lambda x. LOVE y x))
+# which is also of type s;
+syntactic_realisation semantics analyse (SOME WOMAN) (lambda y. (EVERY MAN) (lambda x. LOVE y x)) :s;
+
+# Indeed, these two different syntactic terms have a same syntactic realisation
+# and two different meanings
+
diff --git a/examples/montague.acg b/examples/montague.acg
new file mode 100644
index 0000000000000000000000000000000000000000..0c2dab1d8e8feba59d89fd0860b87d228cf1aba9
--- /dev/null
+++ b/examples/montague.acg
@@ -0,0 +1,107 @@
+(* This files gives an example of how to use the ACG toolkit to illustrate Montague's semantics *)
+
+
+(* First we define the syntactic categories and the syntactic terms *)
+signature syntax =
+	(* the np, s and n tpes *)
+	np,n,s:type;
+
+	(* the syntactic constants that correspond to John and mary *)
+	JOHN,MARY:np;
+
+	(* the one for loves *)
+	LOVE:np -> np -> s;
+
+	(* the one for every and the one for some *)
+
+	EVERY,SOME : n -> (np -> s) -> s;
+
+	(* and the ones for man and woman *)
+
+	MAN,WOMAN : n;
+end
+
+
+(* Then we define the signature contains the strings that will be used
+*)
+
+signature strings =
+	string : type;
+	
+	(* the infix concatenation operator + *)
+	infix + : string -> string -> string;
+
+	(* the empty string e *)
+	e : string;
+
+	(* all the other strings *)
+	John, Mary, loves, every, some, man, woman:string
+end
+
+
+(* The lexicon that associates the string to the syntactic terms *)
+
+lexicon syntactic_realisation (syntax) : strings =
+	(* all the syntactic types are interpreted as strings *)
+	np,n,s:=string;
+
+	JOHN := John;
+	MARY := Mary;
+
+	(* LOVE is interpreted as a function taking two arguments. The first one is the object and the second one is the subject. It returns the concatenation subject+loves+object *)
+	LOVE := lambda o s.s + loves + o;
+
+	EVERY := lambda n P. P (every + n);
+	SOME := lambda n P.P(some + n);
+	
+	MAN := man;
+	WOMAN := woman;
+end
+	
+
+(* Let's now look at the semantics *)
+
+signature logic =
+
+	(* We define the usual types *)
+
+	e,t:type;
+
+	(* Then few non logical-constants *)
+	love:e -> e -> t;
+	j,m:e;
+	man,woman : e->t;
+
+	(* And finally, here are the logical constants *)
+
+	(* Cconjunction *)
+	infix & : t -> t -> t;	
+	
+	(* Implications*)
+	infix > : t -> t -> t;
+
+	(* Quantifiers *)
+	binder All : (e=>t) -> t;
+	binder Ex : (e=>t) -> t;
+
+end
+
+lexicon semantics (syntax) : logic =
+	
+	(* We interpret np as entity, n as properties (s -> t) and of course s as propositions (truth values) *)
+	np := e;
+	n := e -> t;
+	s := t;
+
+	JOHN := j;
+	MARY := m;
+
+	MAN := man;
+	WOMAN := woman;
+	
+	(* Note that we interpret LOVE whose first argument is the object and the second one as a suject using the predicate "love" for which love x y is true whenever x loves y *)
+	LOVE := lambda x y. love y x ;
+	
+	EVERY := lambda P Q.All x. (P x) > (Q x);
+	SOME :=  lambda P Q.Ex x. (P x) & (Q x) ;
+end