<!DOCTYPE html><html><head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
</head>
<body>
<div class="moz-forward-container">
<div>
<div dir="ltr">
<div>Dear all,</div>
<div><br>
</div>
<div>I have been asked to forward the below talk announcement
by MSP alumnus Bruno. Personally I'm looking forward to it!<br>
</div>
<div><br>
</div>
<div>Best wishes,<br>
Fred<br>
</div>
<div>
<br>
<div class="gmail_quote gmail_quote_container">
<div dir="ltr" class="gmail_attr">---------- Forwarded
message ---------<br>
From: <strong class="gmail_sendername" dir="auto">Neil
Ghani</strong> <span dir="auto">
<<a href="mailto:neil@kodamai.com" moz-do-not-send="true" class="moz-txt-link-freetext">neil@kodamai.com</a>></span><br>
Date: Wed, Nov 12, 2025 at 2:06 PM<br>
Subject: Fwd: Talk<br>
To: Riu Sakamoto <<a href="mailto:riu@kodamai.com" moz-do-not-send="true" class="moz-txt-link-freetext">riu@kodamai.com</a>><br>
</div>
<br>
<br>
<div dir="ltr">
<div class="gmail_quote">
<div dir="ltr">
<div>Dear All</div>
<div><br>
</div>
<div>Kodamai is hosting the following talk this
Friday 14 November at 4pm UK time in the general
area of Category Theory and AI. If you are
interested, please contact
<a href="mailto:neil@kodamai.com" target="_blank" moz-do-not-send="true" class="moz-txt-link-freetext">neil@kodamai.com</a>
for the online url
<p><strong>Speaker: Bruno Gavranovic</strong></p>
<p><strong>TensorType: Implementing and extending
Deep Learning with Types</strong></p>
<p>Category theory has seen a rise in applications
in deep learning, bringing with it ideas and
tools from functional programming and dependent
type theory. However, implementing these ideas
in practice faces significant friction because
successful neural network frameworks only exist
in dynamically typed languages such as Python.
Attempts to implement these ideas in
statically-typed languages have struggled with
expressiveness and ergonomics, typically only
replicating what exists without imagining what
can be.</p>
<p>In this talk, I will introduce TensorType, a
tensor processing framework implemented in Idris
2 aiming to demonstrate that ergonomics and
rigor need not be at odds. TensorType provides
tensor operations checked at compile-time while
enabling fundamentally new capabilities: tensors
that branch and recurse instead of being
confined to rectangular shapes. I will walk
through the design choices behind TensorType,
showcase how containers power its core
abstractions, and explore strange new worlds it
enables.<br>
</p>
</div>
</div>
<div dir="ltr" class="gmail_signature">
</div>
</div>
</div>
</div>
</div>
</div>
</div>
</div>
</body>
</html>