diff --git a/utils/cool2tatl.cabal b/utils/cool2tatl.cabal
new file mode 100644
index 0000000000000000000000000000000000000000..049effa27e2939c941f650be51ec46938485418a
--- /dev/null
+++ b/utils/cool2tatl.cabal
@@ -0,0 +1,29 @@
+-- Initial cool2tatl.cabal generated by cabal init.  For further
+-- documentation, see http://haskell.org/cabal/users-guide/
+
+name:                cool2tatl
+version:             0.1.0.0
+-- synopsis:
+-- description:
+license:             PublicDomain
+license-file:        LICENSE
+author:              Daniel Gorín
+maintainer:          jcpetruzza@gmail.com
+-- copyright:
+-- category:
+build-type:          Simple
+-- extra-source-files:
+cabal-version:       >=1.10
+
+executable cool2tatl
+  main-is:            cool2tatl.hs
+  ghc-options:        -Wall -O2
+  -- other-modules:
+  -- other-extensions:
+  build-depends:       base >=4.6 && <4.7
+                      ,parsers
+                      ,parsec
+                      ,transformers
+                      ,bytestring >= 0.10.2.0
+  -- hs-source-dirs:
+  default-language:    Haskell2010
diff --git a/utils/cool2tatl.hs b/utils/cool2tatl.hs
new file mode 100644
index 0000000000000000000000000000000000000000..d831cf3ff6f52e0ce2cc8e7673bcb3c894dd7f2f
--- /dev/null
+++ b/utils/cool2tatl.hs
@@ -0,0 +1,97 @@
+module Main
+
+where
+
+import Control.Applicative
+
+import Data.ByteString.Lazy ( ByteString )
+import qualified Data.ByteString.Lazy.Char8   as BS
+import qualified Data.ByteString.Lazy.Builder as BS
+
+import Data.Char
+import Data.List
+import Data.Monoid
+
+
+import Text.Parser.Combinators
+import Text.Parser.Expression
+import Text.Parser.Token
+import Text.Parser.Token.Style
+import Text.Parsec.Prim ( Parsec, parse )
+
+import System.Environment
+import System.IO
+
+data Fm
+ =
+   Top
+ | Bot
+ | Pro  ByteString
+ | Neg  Fm
+ | Con  Fm Fm
+ | Dis  Fm Fm
+ | Imp  Fm Fm
+ | Dia  [Integer] Fm
+ | Box  [Integer] Fm
+ deriving Show
+
+type P a = Parsec ByteString () a
+
+coolFm :: P Fm
+coolFm = buildExpressionParser table (parens coolFm <|> atom)
+ where
+   table
+    = [ [unaryOp  "~"  Neg]
+      , [binaryOp "&"  Con]
+      , [binaryOp "=>" Con]
+      , [binaryOp "|"  Dis]
+      ]
+
+   unaryOp  s f = Prefix (f <$ symbol s)
+
+   binaryOp s f = Infix  (f <$ symbol s) AssocLeft
+
+   atom
+    = choice [
+       Top <$  symbol "True"
+      ,Bot <$  symbol "False"
+      ,Pro <$> ident emptyIdents
+      ,Dia <$> between (symbol "<{") (symbol "}>") (some natural) <*> coolFm
+      ,Box <$> between (symbol "[{") (symbol "}]") (some natural) <*> coolFm
+      ]
+
+tatlFm :: Fm -> BS.Builder
+tatlFm fm
+ = case fm of
+     Top     -> tatlFm $ Dis p (Neg p)
+     Bot     -> tatlFm $ Con p (Neg p)
+     Pro q   -> BS.lazyByteString q
+     Neg a   -> c '~' <> tatlFm a
+     Con a b -> mconcat [c '(', tatlFm a, s " /\\ ", tatlFm b, c ')']
+     Dis a b -> mconcat [c '(', tatlFm a, s " \\/ ", tatlFm b, c ')']
+     Imp a b -> mconcat [c '(', tatlFm a, s " -> ",  tatlFm b, c ')']
+     Dia g a -> s "<<" <> (mconcat $ intersperse (c ',') $ map i g) <> s ">>X" <> tatlFm a
+     Box g a -> tatlFm (Neg $ Dia g $ Neg a)
+ where
+   s = BS.stringUtf8
+   c = BS.charUtf8
+   i = BS.integerDec
+   p = Pro (BS.pack "p")
+
+ensure :: Integer -> Fm -> Fm
+ensure n fm = Con fm (Dia [n] Top)
+
+main :: IO ()
+main
+ = do args <- getArgs
+      case args of
+        [n] | all isDigit n -> go (read n)
+        _   -> err "Max number of agents expected!"
+
+ where
+  go n
+   = either (err . show) (out . tatlFm . ensure n) . parse coolFm "<stdin>" =<< BS.getContents
+
+  err = hPutStrLn stderr
+
+  out = BS.putStrLn . BS.toLazyByteString