diff --git a/pkgs/applications/science/logic/celf/default.nix b/pkgs/applications/science/logic/celf/default.nix
new file mode 100644
index 000000000000..669cd46cd2ec
--- /dev/null
+++ b/pkgs/applications/science/logic/celf/default.nix
@@ -0,0 +1,36 @@
+{ stdenv, fetchFromGitHub, smlnj }:
+
+stdenv.mkDerivation rec {
+  pname = "celf";
+  pversion = "2013-07-25";
+  name = "${pname}-${pversion}";
+
+  src = fetchFromGitHub {
+    owner  = "clf";
+    repo   = pname;
+    rev    = "d61d95900ab316468ae850fa34a2fe9488bc5b59";
+    sha256 = "0slrwcxglp0sdbp6wr65cdkl5wcap2i0fqxbwqfi1q3cpb6ph6hq";
+  };
+
+  buildInputs = [ smlnj ];
+
+  # (can also build with MLton)
+  buildPhase = ''
+    export SMLNJ_HOME=${smlnj}
+    sml < main-export.sml
+  '';
+
+  installPhase = ''
+    mkdir -p $out/bin
+    cp .heap* $out/bin/
+    ./.mkexec ${smlnj}/bin/sml $out/bin celf
+  '';
+
+  meta = with stdenv.lib; {
+    description = "Linear logic programming system";
+    homepage = http://github.com/clf/celf;
+    license = licenses.gpl3;
+    maintainers = with maintainers; [ bcdarwin ];
+    platforms = platforms.unix;
+  };
+}
diff --git a/pkgs/top-level/all-packages.nix b/pkgs/top-level/all-packages.nix
index a71a4c88726e..88df3cd265ae 100644
--- a/pkgs/top-level/all-packages.nix
+++ b/pkgs/top-level/all-packages.nix
@@ -20265,6 +20265,12 @@ with pkgs;
 
   tptp = callPackage ../applications/science/logic/tptp {};
 
+  celf = callPackage ../applications/science/logic/celf {
+    smlnj = if stdenv.isDarwin
+      then smlnjBootstrap
+      else smlnj;
+  };
+
   twelf = callPackage ../applications/science/logic/twelf {
     smlnj = if stdenv.isDarwin
       then smlnjBootstrap