-
Notifications
You must be signed in to change notification settings - Fork 1
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Deploying to master from @ b9dee10 🚀
- Loading branch information
1 parent
d238f6f
commit a9f7631
Showing
166 changed files
with
233 additions
and
11 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -37,7 +37,6 @@ | |
<main role="main"> | ||
<article> | ||
<section class="header"> | ||
Posted on May 12, 2016 | ||
|
||
</section> | ||
<section> | ||
|
@@ -146,6 +145,9 @@ <h3 id="постскриптум">Постскриптум</h3> | |
возможности работы, напишите мне письмо на | ||
<a href="mailto:[email protected]">[email protected]</a>.</p> | ||
</section> | ||
<p align="right"> | ||
<i>May 12, 2016</i> | ||
</p> | ||
</article> | ||
|
||
</main> | ||
|
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,71 @@ | ||
<!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 - Presenting at TYPES'23</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"> | ||
<article> | ||
<section class="header"> | ||
|
||
</section> | ||
<section> | ||
<p>I gave a talk on <a href="https://types2023.webs.upv.es/">TYPES’23</a> about | ||
implementing rank-polymorphic arrays in dependently-typed theory.</p> | ||
<p>The slides are <a href="../talks/2023-types">available here</a>, and the | ||
extended abstract <a href="../pubs/2023-types-abstract.pdf">can be found here</a> | ||
The abstract follows.</p> | ||
<p>Rank polymorphism is the ability of a function to operate on arrays of | ||
arbitrary ranks. The advantages of rank-polymorphism are twofold: very | ||
generic array combinators and the ability to specify advanced parallel | ||
algorithms such as scan or blocked matrix multiplication in a very | ||
natural combinatorial style. In this work we present an embedding of | ||
rank-polymorphic arrays within a dependently-typed language. Our | ||
embedding offers the generality of the specifications found in array | ||
languages. At the same time, we guarantee safe indexing and offer a way | ||
to reason about concurrency patterns within the given algorithm. The | ||
notion of array reshaping makes it possible to derive multiple parallel | ||
versions of the algorithm from a single specification. The overall | ||
structure of the proposed array framework is surprisingly similar to | ||
categories with families that is often used to encode type theory. | ||
Shapes are contexts, reshapes are substitutions, and arrays are | ||
well-scoped terms.</p> | ||
</section> | ||
<p align="right"> | ||
<i>June 12, 2023</i> | ||
</p> | ||
</article> | ||
|
||
</main> | ||
</body> | ||
</html> |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
Oops, something went wrong.