Recent searches

No recent searches

Search options

Only available when logged in.
shakedown.social is one of the many independent Mastodon servers you can use to participate in the fediverse.
A community for live music fans with roots in the jam scene. Shakedown Social is run by a team of volunteers (led by @clifff and @sethadam1) and funded by donations.

Administered by:

Server stats:

249
active users

shakedown.social: AboutStatusProfiles directoryPrivacy policy

Mastodon: AboutGet the appKeyboard shortcutsView source codev4.4.3

#ITP

0 posts0 participants0 posts today
José A. Alonso<p>A crash course on type theory. ~ Antoine Chambert-Loir. <a href="https://webusers.imj-prg.fr/~antoine.chambert-loir/exposes/accitt.pdf" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">webusers.imj-prg.fr/~antoine.c</span><span class="invisible">hambert-loir/exposes/accitt.pdf</span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>LeanProver</span></a> <a href="https://mathstodon.xyz/tags/TypeTheory" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>TypeTheory</span></a></p>
José A. Alonso<p>Scaling mathematical reasoning through data, tools, and generative selection. ~ Ivan Moshkov et als. <a href="https://openreview.net/forum?id=OM7ZN0PmSS" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">openreview.net/forum?id=OM7ZN0</span><span class="invisible">PmSS</span></a> <a href="https://mathstodon.xyz/tags/LLMs" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>LLMs</span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>LeanProver</span></a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Math</span></a></p>
José A. Alonso<p>A formalization of elementary linear algebra: Part I. ~ David M. Russinoff. <a href="https://www.russinoff.com/papers/linear1.pdf" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://www.</span><span class="ellipsis">russinoff.com/papers/linear1.p</span><span class="invisible">df</span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/ACL2" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>ACL2</span></a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Math</span></a></p>
José A. Alonso<p>Ordinal exponentiation in homotopy type theory. ~ Tom de Jong, Nicolai Kraus, Fredrik Nordvall Forsberg, Chuangjie Xu. <a href="https://arxiv.org/abs/2501.14542" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="">arxiv.org/abs/2501.14542</span><span class="invisible"></span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/Agda" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Agda</span></a> <a href="https://mathstodon.xyz/tags/HoTT" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>HoTT</span></a></p>
Rob Sison<p>There's now a video up of the talk I gave at this year's seL4 Summit, on the status of UNSW's projects to verify Time Protection and Microkit-based userland OS services for the seL4 microkernel:</p><p><a href="https://youtu.be/7wcFx6OTEL4" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="">youtu.be/7wcFx6OTEL4</span><span class="invisible"></span></a></p><p><a href="https://aus.social/tags/sel4summit" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>sel4summit</span></a> <a href="https://aus.social/tags/seL4" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>seL4</span></a> <a href="https://aus.social/tags/verification" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>verification</span></a> <a href="https://aus.social/tags/operatingsystems" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>operatingsystems</span></a> <a href="https://aus.social/tags/microkernel" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>microkernel</span></a> <a href="https://aus.social/tags/IsabelleHOL" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>IsabelleHOL</span></a> <a href="https://aus.social/tags/HOL4" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>HOL4</span></a> <a href="https://aus.social/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>ITP</span></a> <a href="https://aus.social/tags/modelchecking" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>modelchecking</span></a> <a href="https://aus.social/tags/formalmethods" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>formalmethods</span></a> <a href="https://aus.social/tags/formalverification" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>formalverification</span></a> <a href="https://aus.social/tags/formal_methods" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>formal_methods</span></a> <a href="https://aus.social/tags/formal_verification" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>formal_verification</span></a></p>
Kilroy_Was_Here<p>PSA:</p><p>Please <a href="https://dobbs.town/tags/donate" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>donate</span></a> <a href="https://dobbs.town/tags/blood" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>blood</span></a> .</p><p>I have a very rare autoimmune disorder that causes my body to attack blood platelets. It's called <a href="https://dobbs.town/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>ITP</span></a>. </p><p>A routine blood test two days ago revealed that my blood platelets were dangerously low. If you don't know, blood platelets are what make you stop bleeding when you have any injury that causes bleeding.</p><p>I was scheduled for an emergency platelet transfusion. They couldn't give it to me because there's a critical platelet shortage.</p><p>Again, please donate blood.</p>
AgaposteMom (She/Her)<p>I am recovering from <a href="https://mastodon.social/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>ITP</span></a> (immune system kills your own platelets disease), I was in the hospital all last week. But I am now putting on a mask, pumped up on steroids, to run to the store to buy supplies/porch drop for my sister and 80 yrs old parents who came down with COVID today. <br><a href="https://mastodon.social/tags/Ottawa" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Ottawa</span></a> <a href="https://mastodon.social/tags/CovidIsEverywhere" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>CovidIsEverywhere</span></a> <a href="https://mastodon.social/tags/MaskUp" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>MaskUp</span></a> <a href="https://mastodon.social/tags/WearAMask" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>WearAMask</span></a> <a href="https://mastodon.social/tags/CovidIsNotOver" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>CovidIsNotOver</span></a></p><p><a href="https://mastodon.social/tags/ThisWasSupposeToBeAboutMeCovid" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>ThisWasSupposeToBeAboutMeCovid</span></a></p>
RanaldClouston<p>I'm enjoying the <a href="https://fediscience.org/tags/Pittsposium" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Pittsposium</span></a> in <a href="https://fediscience.org/tags/Cambridge" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Cambridge</span></a> , a workshop in honour of my PhD supervisor Andy Pitts. Loved this talk by Larry Paulson, who advocated for mathematicians to use proof assistants with liberal use of sorry / admitted for parts of proofs they are confident in to avoid burning time on small details, for example the many lines of code required when verifying one sentence proofs in a standard textbook. <a href="https://fediscience.org/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>ITP</span></a></p>
José A. Alonso<p><a href="https://mathstodon.xyz/tags/Calculemus" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Calculemus</span></a>: Demostraciones con Lean4: "Si G es un grupo y a, b ∈ G, tales que ab = 1 entonces a⁻¹ = b". <a href="https://www.glc.us.es/~jalonso/calculemus/21-ago-23/" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://www.</span><span class="ellipsis">glc.us.es/~jalonso/calculemus/</span><span class="invisible">21-ago-23/</span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/Lean4" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Lean4</span></a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Math</span></a></p>
TrendingLive feeds
About