Deploying to master from @ 76dc191 🚀

ashinkarov · Jul 30, 2023 · 75dd36a · 75dd36a
1 parent a9f7631
commit 75dd36a
Show file tree

Hide file tree

Showing 26 changed files with 116 additions and 0 deletions.
diff --git a/bib.bib b/bib.bib
@@ -1,3 +1,27 @@
+@InProceedings{2022-types,
+	author = {Altenkirch, Thorsten and Kaposi, Ambrus and \v{S}inkarovs, Artjoms and V\'{e}gh, Tam\'{a}s},
+	title = {{The M\"{u}nchhausen Method in Type Theory}},
+	booktitle = {28th International Conference on Types for Proofs and Programs (TYPES 2022)},
+	pages = {10:1--10:20},
+	series = {Leibniz International Proceedings in Informatics (LIPIcs)},
+	isbn = {978-3-95977-285-3},
+	issn = {1868-8969},
+	year = {2023},
+	volume = {269},
+	editor = {Kesner, Delia and P\'{e}drot, Pierre-Marie},
+	publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
+	address = {Dagstuhl, Germany},
+	url = {/pubs/2022-types.pdf},
+	urn = {urn:nbn:de:0030-drops-184534},
+	doi = {10.4230/LIPIcs.TYPES.2022.10},
+	annote = {Keywords: type theory, proof assistants, very dependent types},
+	date = {2023-07-28},
+	addinfo = {
+    The sources of the paper with the code
+    \href{https://bitbucket.org/akaposi/combinator/src/master/post-types2022/}{are available here}.
+    Here is \href{https://drops.dagstuhl.de/opus/volltexte/2023/18453}{the official link to the published paper}.
+  }}
+
 @InProceedings{2023-fscd,
 	author = {Altenkirch, Thorsten and 
             Kaposi, Ambrus and

diff --git a/publications.html b/publications.html
@@ -37,6 +37,11 @@
         <main role="main">
             <ul>
 
+<li>2023
+ <a href="./pubs/2022-types.html">The Münchhausen Method in Type Theory
+</a></li>
+
+
 <li>2023
  <a href="./pubs/2023-fscd.html">Combinatory Logic and Lambda Calculus Are Equal, Algebraically
 </a></li>

diff --git a/pubs/2018-ifl-memreuse.png b/pubs/2018-ifl-memreuse.png
diff --git a/pubs/2018-max-resilience.png b/pubs/2018-max-resilience.png
diff --git a/pubs/2019-conv-apl.png b/pubs/2019-conv-apl.png
diff --git a/pubs/2019-ifl-tensorcomp.png b/pubs/2019-ifl-tensorcomp.png
diff --git a/pubs/2019-max-resilience.png b/pubs/2019-max-resilience.png
diff --git a/pubs/2020-msfp.png b/pubs/2020-msfp.png
diff --git a/pubs/2021-cnn.png b/pubs/2021-cnn.png
diff --git a/pubs/2021-extraction.png b/pubs/2021-extraction.png
diff --git a/pubs/2021-gpce.png b/pubs/2021-gpce.png
diff --git a/pubs/2022-scan.png b/pubs/2022-scan.png
diff --git a/pubs/2022-types.html b/pubs/2022-types.html
@@ -0,0 +1,87 @@
+<!doctype html>
+<html lang="en">
+    <head>
+        <meta charset="utf-8">
+        <meta http-equiv="x-ua-compatible" content="ie=edge">
+        <meta name="viewport" content="width=device-width, initial-scale=1">
+        <title>Artem Shinkarov - 2022-types</title>
+        <link rel="stylesheet" href="../css/notosans.css" />
+        <link rel="stylesheet" href="../css/merriweather.css" />
+        <link rel="stylesheet" href="../css/sakura.css" />
+        <link rel="stylesheet" href="../css/tema.css" />
+    </head>
+    <script>
+      function visibilityToggle(id) {
+         var x = document.getElementById(id);
+         //alert("display of " + id + " = " + x.style.display)
+         if (x.style.display === "none") {
+           x.style.display = "block";
+         } else {
+           x.style.display = "none";
+         }
+      }
+    </script>
+    <body>
+        <header>
+            <div class="logo">
+                <a href="../">Artem Shinkarov</a>
+            </div>
+            <nav>
+                <a href="../">About</a>
+                <a href="../publications.html">Publications</a>
+                <a href="../archive.html">Posts</a>
+                <a href="../links.html">Links</a>
+            </nav>
+        </header>
+        <hr style="border:1px solid #e4e4e4;" />
+        <main role="main">
+            <div class="paper-img-desc">
+  <a class="paper-img" href="../pubs/2022-types.pdf
+">
+
+    <img src="../pubs/2022-types.png" style="width:30rem">
+
+  </a>
+  <h2>The Münchhausen Method in Type Theory
+</h2>
+
+  <p>T. Altenkirch, A. Kaposi, A. Šinkarovs, and T. Végh, <span>“<span class="nocase">The Münchhausen Method in Type Theory</span>,”</span> in
+<em>28th international conference on types for proofs and programs
+(TYPES 2022)</em>, Jul. 2023, vol. 269, pp. 10:1–10:20. doi: <a href="https://doi.org/10.4230/LIPIcs.TYPES.2022.10">10.4230/LIPIcs.TYPES.2022.10</a>.</p>
+
+  <p class="bibpdf">
+    <a href="../pubs/2022-types.pdf
+">[URL]</a>
+    <a href="javascript:visibilityToggle('bibtex-box');">[BibTeX]</a>
+  </p>
+</div>
+
+<code class="bibinfo" id="bibtex-box" style="display:none;">@InProceedings{2022-types,
+	author = {Altenkirch, Thorsten and Kaposi, Ambrus and \v{S}inkarovs, Artjoms and V\'{e}gh, Tam\'{a}s},
+	title = {{The M\"{u}nchhausen Method in Type Theory}},
+	booktitle = {28th International Conference on Types for Proofs and Programs (TYPES 2022)},
+	pages = {10:1--10:20},
+	series = {Leibniz International Proceedings in Informatics (LIPIcs)},
+	isbn = {978-3-95977-285-3},
+	issn = {1868-8969},
+	year = {2023},
+	volume = {269},
+	editor = {Kesner, Delia and P\'{e}drot, Pierre-Marie},
+	publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
+	address = {Dagstuhl, Germany},
+	urn = {urn:nbn:de:0030-drops-184534},
+	doi = {10.4230/LIPIcs.TYPES.2022.10},
+	annote = {Keywords: type theory, proof assistants, very dependent types}}</code>
+
+
+
+
+<h2>Additional Information</h2>
+<p><p><span> The sources of the paper with the code <a href="https://bitbucket.org/akaposi/combinator/src/master/post-types2022/">are
+available here</a>. Here is <a href="https://drops.dagstuhl.de/opus/volltexte/2023/18453">the official
+link to the published paper</a>. </span></p></p>
+
+
+        </main>
+    </body>
+</html>
diff --git a/pubs/2022-types.pdf b/pubs/2022-types.pdf
diff --git a/pubs/2022-types.png b/pubs/2022-types.png
diff --git a/pubs/2023-fscd.png b/pubs/2023-fscd.png
diff --git a/pubs/array-comp.png b/pubs/array-comp.png
diff --git a/pubs/asv-thesis.png b/pubs/asv-thesis.png
diff --git a/pubs/bgs-fortran.png b/pubs/bgs-fortran.png
diff --git a/pubs/ccpe-data-layouts.png b/pubs/ccpe-data-layouts.png
diff --git a/pubs/cpcgcc.png b/pubs/cpcgcc.png
diff --git a/pubs/data-layouts.png b/pubs/data-layouts.png
diff --git a/pubs/layout-correctness.png b/pubs/layout-correctness.png
diff --git a/pubs/rosetta-stone.png b/pubs/rosetta-stone.png
diff --git a/pubs/sexynbody.png b/pubs/sexynbody.png
diff --git a/pubs/transfinite.png b/pubs/transfinite.png