Skip to content
Find file
Fetching contributors…
Cannot retrieve contributors at this time
207 lines (145 sloc) 10.5 KB
<!DOCTYPE html>
<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8" />
<meta name="readability-verification" content="cG3MqZcEVveKZ6mnEFkePAL3Ug79Jxxp5Fn27CM7" />
<title>JS ≫ Notes from Jon Sterling Thought</title>
<link rel="stylesheet" type="text/css" href="./fonts/cmun-sans.css" />
<link rel="stylesheet" type="text/css" href="./fonts/cmun-serif.css" />
<link rel="stylesheet" type="text/css" href="./fonts/cmun-serif-slanted.css" />
<link rel="stylesheet" type="text/css" href="./css/screen.css" />
<link rel="stylesheet" type="text/css" href="./css/syntax.css" />
<link rel="stylesheet" type="text/css" href="./css/coqdoc.css" />
<script type="text/javascript" src="http://code.jquery.com/jquery-1.8.3.min.js"></script>
<link rel="alternate" type="application/rss+xml" title="Jonathan Sterling" href="./rss.xml" />
<!--[if IE]>
<script src="http://html5shiv.googlecode.com/svn/trunk/html5.js"></script><![endif]-->
<!--[if lte IE 7]>
<script src="js/IE8.js" type="text/javascript"></script><![endif]-->
<!--[if lt IE 7]>
<link rel="stylesheet" type="text/css" media="all" href="css/ie6.css"/><![endif]-->
<script type="text/javascript" src="http://cdn.mathjax.org/mathjax/latest/MathJax.js?config=TeX-AMS-MML_HTMLorMML">
MathJax.Hub.Config({
showMathMenu: false,
showProcessingMessages: false,
messageStyle: "none",
'HTML-CSS': {
availableFonts: [],
webFont: 'TeX',
},
TeX: {
extensions: ["color.js", "AMScd.js"],
Macros: {
gk: ["\\style{font-family:Junicode!important; font-size:1.3em;}{\\text{#1}}", 1]
}
}
});
</script>
</head>
<body>
<header>
<h1><a href="./index.html"><span class="title">Notes from Jon Sterling Thought.</span></a></h1>
<!-- <div class="author">Jonathan M. Sterling</div> -->
</header>
<section id="about">
<p>Marxist-Leninist Type Theorist @ CMU and student of ancient languages. I co-host <a href="http://typetheorypodcast.com/">The Type Theory Podcast</a>, and created the <a href="http://www.redprl.org/">RedPRL</a> proof assistant. Ideas written up here are rough at best.</p>
<ul class="links">
<li><a href="./archive.html">Archives</a></li>
<li><a href="./talks.html">Talks</a></li>
<li><a href="./papers.html">Papers</a></li>
</ul>
</section>
<section>
<article class="digest">
<h3>
<a href="./posts/2016-06-22-dialectics-in-mathematics.html">Some Remarks on Dialectics in Mathematics</a>
<span class="date">June 22, 2016</span>
</h3>
<p><em>Dialectical materialism</em>, far from being merely the definitive theory of political and historical movement, also serves as the guiding light for the progressive mathematician in its manifestation as the science of adjoint functors in category theory.</p>
<p>As Lawvere stated in his influential note <em>Quantifiers and Sheaves</em>, the essential move in mathematics is to identify the principal contradictions of a theory in the form of pairs of adjoint functors, and to “weaponize” them as slogans to drive the further development (and generalization) of the thing. In this note, I would like to make a few remarks about the pervasiveness of dialectical phenomena, both in the mathematics itself as well as in the practical engagement in mathematical activity.</p>
<div class="read_more">
<a href="./posts/2016-06-22-dialectics-in-mathematics.html"> more &hellip;</a>
</div>
</article>
<article class="digest">
<h3>
<a href="./posts/2015-07-05-spreads-fans-and-bars-over-containers.html">Spreads, Fans and Bars over Containers</a>
<span class="date">July 5, 2015</span>
</h3>
<p>This post is an introduction to the container-oriented generalization of the core Brouwerian (co)data structures, inspired by Ghani, Hancock and Pattinson.<a href="#fn1" class="footnoteRef" id="fnref1"><sup>1</sup></a> I am not introducing anything novel; I’m merely taking their framework and showing how to round up the usual suspects of Brouwerian mathematics in their generalized, “family-friendly” setting. I am using Constable et al’s Computational Type Theory + Induction-Recursion as my metalanguage,<a href="#fn2" class="footnoteRef" id="fnref2"><sup>2</sup></a> but other variants of type theory may be used as well.</p>
<div class="read_more">
<a href="./posts/2015-07-05-spreads-fans-and-bars-over-containers.html"> more &hellip;</a>
</div>
</article>
<article class="digest">
<h3>
<a href="./posts/2015-07-03-modernized-lcf-the-logic-of-goals-and-tactics.html">Modernized LCF: The Logic of Goals and Tactics</a>
<span class="date">July 3, 2015</span>
</h3>
<p>Here, I present a judgemental reconstruction of LCF-style tactic systems, called <strong>Modernized LCF</strong>, which admits various extensions including <em>validations</em> (checkable certificates). The purpose is to present the structure and meaning of refinement proof directly as a logical theory with a meaning explanation, in contrast to the standard practice of taking refinement proof as an extra-logical “finishing touch”.</p>
<div class="read_more">
<a href="./posts/2015-07-03-modernized-lcf-the-logic-of-goals-and-tactics.html"> more &hellip;</a>
</div>
</article>
<article class="digest">
<h3>
<a href="./posts/2015-06-27-oplss-2015-retrospective.html">Oregon Programming Languages Summer School, 2015</a>
<span class="date">June 27, 2015</span>
</h3>
<p>This year’s <a href="https://www.cs.uoregon.edu/research/summerschool/summer15/">Oregon Programming Languages Summer School</a>, organized by Bob Harper, Greg Morrisett and Zena Ariola, has come to a close after two amazing weeks. I wanted to take a moment to thank everyone who made my time here so pleasant, with special regards to Bob Harper and Mark Bickford, who patiently answered my numerous questions about Nuprl and Brouwerian mathematics.</p>
<div class="read_more">
<a href="./posts/2015-06-27-oplss-2015-retrospective.html"> more &hellip;</a>
</div>
</article>
<article class="digest">
<h3>
<a href="./posts/2015-06-14-functionality-mutability-non-determinism.html">Functionality, Mutability &amp; Non-Determinism in Type Theory</a>
<span class="date">June 14, 2015</span>
</h3>
<p>Recent conversations have convinced me that there are several misconceptions about the status of side effects in a type theoretic setting, and how to reason about their benignity. Briefly, I will clarify this matter by proposing how one might go about integrating free assignables and non-determinism into Computational Type Theory.<a href="#fn1" class="footnoteRef" id="fnref1"><sup>1</sup></a> I do not answer all questions raised by this proposal, but I intend to be provocative and suggest a rough path toward realizing this goal.</p>
<div class="read_more">
<a href="./posts/2015-06-14-functionality-mutability-non-determinism.html"> more &hellip;</a>
</div>
</article>
<article class="digest">
<h3>
<a href="./posts/2015-04-24-note-on-diaconescus-theorem.html">Note on Diaconescu’s Theorem</a>
<span class="date">April 24, 2015</span>
</h3>
<p>Briefly, Diaconescu’s theorem states that the axiom of choice &amp; extensionality together suffice to imply the principle of the excluded middle (PEM). In <a href="https://people.kth.se/~kurlberg/colloquium/2005/MartinLooef.pdf"><em>100 Years of Zermelo’s Axiom of Choice</em></a>, Martin-Löf distinguishes an intensional version of AC from an extensional one, and argues that whilst the former is a theorem of intuitionistic type theory, the latter leads to taboo. In this note, I hope to clarify a few matters, and demonstrate that the matter at hand is not so much extensionality, but infelicitous interpretation of quantifiers. When viewed through this lens, it becomes evident that the problem all along was setoids, not extensionality.</p>
<div class="read_more">
<a href="./posts/2015-04-24-note-on-diaconescus-theorem.html"> more &hellip;</a>
</div>
</article>
<article class="digest">
<h3>
<a href="./posts/2015-04-18-a-higher-order-approach-to-explicit-contexts-in-lf.html">A Higher-Order Approach to Explicit Contexts in LF</a>
<span class="date">April 18, 2015</span>
</h3>
<p>There are two standard techniques for representing dependently typed calculi in the LF. The first is to re-use the LF contexts for the object contexts, which can lead to difficulties when the meaning of hypothetico-general judgement in the object language is stronger than in the LF; this is, for instance, the case in MLTT 1979, where non-trivial functionality obligations are incurred in the sequent judgement.</p>
<p>Another technique advanced by Crary is to represent contexts explicitly, and then define a sequent judgement over them; this can be used to resolve the problem described above (and several others), but it comes at the cost of verbosity, and introduces certain other difficulties for my purpose. In this paper, I demonstrate an alternative, higher-order encoding of telescopes which can be used to faithfully encode the functional sequent judgement for MLTT 1979. You may also view a parallel <a href="https://github.com/jonsterling/twelf-cmcp">Twelf development</a>.</p>
<div class="read_more">
<a href="./posts/2015-04-18-a-higher-order-approach-to-explicit-contexts-in-lf.html"> more &hellip;</a>
</div>
</article>
<article class="digest">
<h3>
<a href="./posts/2014-10-29-proof-term-assignments-and-intuitionistic-truth.html">Proof Term Assignments and Intuitionistic Truth</a>
<span class="date">October 29, 2014</span>
</h3>
<p>In 1994, Per Martin-Löf wrote <a href="https://github.com/michaelt/martin-lof/blob/master/pdfs/Martin-Lof-Analytic-and-Synthetic-Judgements-in-Type-Theory.pdf">Analytic and Synthetic Judgement in Type Theory</a>, in which he convincingly showed that undecidability phenomena should be understood in terms of synthetic judgement, and demonstrated how the judgements of one theory may be made the propositions of another.</p>
<div class="read_more">
<a href="./posts/2014-10-29-proof-term-assignments-and-intuitionistic-truth.html"> more &hellip;</a>
</div>
</article>
<p>
<a href="./archive.html">All posts&hellip;</a>
</p>
</section>
<script src="//static.getclicky.com/js" type="text/javascript"></script>
<script type="text/javascript">try{ clicky.init(66625087);
}catch(e){}</script>
<noscript><p><img alt="Clicky" width="1" height="1" src="//in.getclicky.com/66625087ns.gif" /></p></noscript>
<a rel="me" href="http://twitter.com/jonsterling"></a>
</body>
</html>
Something went wrong with that request. Please try again.