diff --git a/.gitignore b/.gitignore
index 74d3949..93424b3 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,3 +1,5 @@
 _build
 pieuvre
 main.native
+
+*.kate-swp
diff --git a/main.ml b/main.ml
index e69de29..8ff999d 100644
--- a/main.ml
+++ b/main.ml
@@ -0,0 +1,2 @@
+open Struct
+open Pieuvre
diff --git a/pieuvre.ml b/pieuvre.ml
index e69de29..7b887dc 100644
--- a/pieuvre.ml
+++ b/pieuvre.ml
@@ -0,0 +1,28 @@
+open Structs
+
+exception TODOException;;
+
+(* Affiche un λ-terme avec la même syntaxe qu’en entrée *)
+let affiche_lam (l: lam) : unit =
+    raise TODOException
+;;
+
+(* Teste si les deux λ-termes l1 et l2 sont α-convertibles *)
+let alpha (l1: lam) (l2: lam) : bool =
+    raise TODOException
+;;
+
+(* Fait un pas de β-réduction, et renvoie None si on a une forme normale *)
+let betastep (l: lam) : lam option =
+    raise TODOException
+;;
+
+(* Affiche les réductions du λ-terme l jusqu’à atteindre une forme normale, ou part en boucle infinie *)
+let reduce (l:lam) : unit =
+    raise TODOException
+;;
+
+(* Vérifie que le λ-terme l sous l'environnement env a bien le type t *)
+let typecheck (env: gam) (l: lam) (t: ty) : bool =
+    raise TODOException
+;;
diff --git a/struct.ml b/struct.ml
deleted file mode 100644
index e69de29..0000000
diff --git a/structs.ml b/structs.ml
new file mode 100644
index 0000000..5884272
--- /dev/null
+++ b/structs.ml
@@ -0,0 +1,16 @@
+(* Variables des λ-termes *)
+type var = string;;
+(* Variable des types simples *)
+type tvar = string;;
+
+(* Type complexe *)
+type ty = TSimple of tvar | TImpl of ty * ty | TFalse;;
+
+(* λ-terme *)
+type lam = LFun of var * ty * lam | LApp of lam * lam | LVar of var | LExf of lam * ty;;
+
+(* Environnement de typage *)
+type gam = (tvar * ty) list;;
+
+(* λ-terme avec des trous *)
+type lho = (lam list) -> lam;;