diff --git a/pkgs/applications/science/logic/jonprl/default.nix b/pkgs/applications/science/logic/jonprl/default.nix
new file mode 100644
index 00000000000..77d617467b4
--- /dev/null
+++ b/pkgs/applications/science/logic/jonprl/default.nix
@@ -0,0 +1,34 @@
+{ fetchgit, stdenv, smlnj, which }:
+
+stdenv.mkDerivation rec {
+  name = "JonPRL";
+  version = "v0.1.0";
+
+  src = fetchgit {
+    url = "https://github.com/jonsterling/JonPRL.git";
+    deepClone = true;
+    rev = "refs/tags/${version}";
+    sha256 = "1z0d8dq1nb4dycic58nnk617hbfgafz0vmwr8gkl0i6405gfg1zy";
+  };
+
+  buildInputs = [ smlnj which ];
+
+  installPhase = ''
+    mkdir -p "$out/bin"
+    cp bin/.heapimg.* "$out/bin/"
+    build/mkexec.sh "${smlnj}/bin/sml" "$out" jonprl
+  '';
+
+  meta = {
+    description = "Proof Refinement Logic - Computational Type Theory";
+    longDescription = ''
+      An proof refinement logic for computational type theory
+      based on Brouwer-realizability & meaning explanations.
+      Inspired by Nuprl
+    '';
+    homepage = http://www.jonprl.org/;
+    license = stdenv.lib.licenses.mit;
+    maintainers = with stdenv.lib.maintainers; [ puffnfresh ];
+    platforms = stdenv.lib.platforms.unix;
+  };
+}
diff --git a/pkgs/top-level/all-packages.nix b/pkgs/top-level/all-packages.nix
index 2d5acc357fe..cd67649f507 100644
--- a/pkgs/top-level/all-packages.nix
+++ b/pkgs/top-level/all-packages.nix
@@ -14560,6 +14560,12 @@ let
 
   iprover = callPackage ../applications/science/logic/iprover {};
 
+  JonPRL = callPackage ../applications/science/logic/jonprl {
+    smlnj = if stdenv.isDarwin
+      then smlnjBootstrap
+      else smlnj;
+  };
+
   lean = callPackage ../applications/science/logic/lean {};
 
   leo2 = callPackage ../applications/science/logic/leo2 {};