<?xml version="1.0" encoding="utf-8"?>
<rss version="2.0"
	xmlns:content="http://purl.org/rss/1.0/modules/content/"
	xmlns:wfw="http://wellformedweb.org/CommentAPI/"
	xmlns:dc="http://purl.org/dc/elements/1.1/"
	xmlns:atom="http://www.w3.org/2005/Atom"
	xmlns:sy="http://purl.org/rss/1.0/modules/syndication/"
	xmlns:slash="http://purl.org/rss/1.0/modules/slash/"
	>

<channel>
	<title>Epilogue</title>
	<atom:link href="http://www.e-pig.org/epilogue/?feed=rss2" rel="self" type="application/rss+xml" />
	<link>http://www.e-pig.org/epilogue</link>
	<description>for Epigram</description>
	<lastBuildDate>Fri, 20 Aug 2010 14:49:51 +0000</lastBuildDate>
	<generator>http://wordpress.org/?v=2.8.4</generator>
	<language>en</language>
	<sy:updatePeriod>hourly</sy:updatePeriod>
	<sy:updateFrequency>1</sy:updateFrequency>
			<item>
		<title>The Art of the Possible</title>
		<link>http://www.e-pig.org/epilogue/?p=683</link>
		<comments>http://www.e-pig.org/epilogue/?p=683#comments</comments>
		<pubDate>Fri, 20 Aug 2010 09:49:08 +0000</pubDate>
		<dc:creator>Adam</dc:creator>
				<category><![CDATA[General]]></category>

		<guid isPermaLink="false">http://www.e-pig.org/epilogue/?p=683</guid>
		<description><![CDATA[Over the last few weeks, there have been some changes to Epigram that make programming in the command-line interface slightly more pleasant. We are starting to think about a high-level language, but in the meantime, I thought it would be nice to look at what sort of programming is possible today. None of this is [...]]]></description>
		<wfw:commentRss>http://www.e-pig.org/epilogue/?feed=rss2&amp;p=683</wfw:commentRss>
		<slash:comments>0</slash:comments>
		</item>
		<item>
		<title>No Representation without Taxation</title>
		<link>http://www.e-pig.org/epilogue/?p=657</link>
		<comments>http://www.e-pig.org/epilogue/?p=657#comments</comments>
		<pubDate>Mon, 31 May 2010 11:31:28 +0000</pubDate>
		<dc:creator>Conor</dc:creator>
				<category><![CDATA[General]]></category>

		<guid isPermaLink="false">http://www.e-pig.org/epilogue/?p=657</guid>
		<description><![CDATA[I think we&#8217;re at a point where we need to question our term/value representation technology. That&#8217;s not to say we need to change it, but we should look at where things are getting a bit out of hand and ask if there&#8217;s anything we can do. The system is not so large that&#8230;actually, it&#8217;s small. [...]]]></description>
		<wfw:commentRss>http://www.e-pig.org/epilogue/?feed=rss2&amp;p=657</wfw:commentRss>
		<slash:comments>3</slash:comments>
		</item>
		<item>
		<title>The Battered Ornaments</title>
		<link>http://www.e-pig.org/epilogue/?p=577</link>
		<comments>http://www.e-pig.org/epilogue/?p=577#comments</comments>
		<pubDate>Mon, 24 May 2010 21:33:45 +0000</pubDate>
		<dc:creator>Conor</dc:creator>
				<category><![CDATA[General]]></category>

		<guid isPermaLink="false">http://www.e-pig.org/epilogue/?p=577</guid>
		<description><![CDATA[Here&#8217;s a story I&#8217;ve had on the go for a while. 
It&#8217;s an experiment in managing the multitudinous variations on the theme of a datatype, inspired by this overlay from a talk I gave ten years ago. If you squint hard at it, you can see that it shows the difference between lists and vectors. [...]]]></description>
		<wfw:commentRss>http://www.e-pig.org/epilogue/?feed=rss2&amp;p=577</wfw:commentRss>
		<slash:comments>0</slash:comments>
		</item>
		<item>
		<title>EPIG, a journey in Quotation</title>
		<link>http://www.e-pig.org/epilogue/?p=504</link>
		<comments>http://www.e-pig.org/epilogue/?p=504#comments</comments>
		<pubDate>Mon, 10 May 2010 22:10:07 +0000</pubDate>
		<dc:creator>pedagand</dc:creator>
				<category><![CDATA[General]]></category>

		<guid isPermaLink="false">http://www.e-pig.org/epilogue/?p=504</guid>
		<description><![CDATA[In this post, I talk about the computation of normal forms in Epigram. Quotation is a key step of normalization, doing some rather exciting magic.
Setting the scene
This post tells a story about terms. We shall discover that some classes of term are more desirable than others. Let us have a look at the battlefield. We [...]]]></description>
		<wfw:commentRss>http://www.e-pig.org/epilogue/?feed=rss2&amp;p=504</wfw:commentRss>
		<slash:comments>7</slash:comments>
		</item>
		<item>
		<title>A bit of infrastructure</title>
		<link>http://www.e-pig.org/epilogue/?p=497</link>
		<comments>http://www.e-pig.org/epilogue/?p=497#comments</comments>
		<pubDate>Sat, 24 Apr 2010 10:48:37 +0000</pubDate>
		<dc:creator>pedagand</dc:creator>
				<category><![CDATA[General]]></category>

		<guid isPermaLink="false">http://www.e-pig.org/epilogue/?p=497</guid>
		<description><![CDATA[I thought I would write a line or two about some recently acquired infrastructure.
Weeks ago, we had left our ivory tower, or rather, our beloved Livingstone tower for a gig in Oxford. Lot of fun, lot of adjunctions. But also a surprising discovery: we met some people who had pulled Epigram source code and actually [...]]]></description>
		<wfw:commentRss>http://www.e-pig.org/epilogue/?feed=rss2&amp;p=497</wfw:commentRss>
		<slash:comments>0</slash:comments>
		</item>
		<item>
		<title>Prop?</title>
		<link>http://www.e-pig.org/epilogue/?p=469</link>
		<comments>http://www.e-pig.org/epilogue/?p=469#comments</comments>
		<pubDate>Sun, 18 Apr 2010 15:30:05 +0000</pubDate>
		<dc:creator>Conor</dc:creator>
				<category><![CDATA[General]]></category>

		<guid isPermaLink="false">http://www.e-pig.org/epilogue/?p=469</guid>
		<description><![CDATA[Let me try to make a bit of high-level sense about Prop in Epigram 2. It&#8217;s quite different from Prop in Coq, it does a different job, and it sits in quite a delicate niche.
Firstly, Prop is explicitly a subuniverse of Set. If P is a Prop, then :- P is the set of its [...]]]></description>
		<wfw:commentRss>http://www.e-pig.org/epilogue/?feed=rss2&amp;p=469</wfw:commentRss>
		<slash:comments>0</slash:comments>
		</item>
		<item>
		<title>Coinduction, observationally</title>
		<link>http://www.e-pig.org/epilogue/?p=418</link>
		<comments>http://www.e-pig.org/epilogue/?p=418#comments</comments>
		<pubDate>Mon, 22 Mar 2010 17:51:27 +0000</pubDate>
		<dc:creator>Conor</dc:creator>
				<category><![CDATA[Observational Type Theory]]></category>

		<guid isPermaLink="false">http://www.e-pig.org/epilogue/?p=418</guid>
		<description><![CDATA[I thought I might report a bit about what I&#8217;ve been up to with coinduction. Headline: we can set up propositional equality so that every coprogram equals its unfolding, even though that had jolly well better not hold definitionally if we want decidable anything.
What I&#8217;ve got is an Agda universe with inductive and coinductive Petersson-Synek [...]]]></description>
		<wfw:commentRss>http://www.e-pig.org/epilogue/?feed=rss2&amp;p=418</wfw:commentRss>
		<slash:comments>5</slash:comments>
		</item>
		<item>
		<title>W-types: good news and bad news</title>
		<link>http://www.e-pig.org/epilogue/?p=324</link>
		<comments>http://www.e-pig.org/epilogue/?p=324#comments</comments>
		<pubDate>Sun, 07 Mar 2010 21:50:45 +0000</pubDate>
		<dc:creator>Conor</dc:creator>
				<category><![CDATA[General]]></category>
		<category><![CDATA[Observational Type Theory]]></category>

		<guid isPermaLink="false">http://www.e-pig.org/epilogue/?p=324</guid>
		<description><![CDATA[I thought I&#8217;d just collect together some disparate observations about W-types, and their use in encoding other recursive datatypes. My motivation, bluntly, is to point out the inevitable unsuitability of W-types as the basis for recursive datatypes in an implementation of decidable type theories. I don&#8217;t want to downplay the conceptual importance of W-types as [...]]]></description>
		<wfw:commentRss>http://www.e-pig.org/epilogue/?feed=rss2&amp;p=324</wfw:commentRss>
		<slash:comments>5</slash:comments>
		</item>
		<item>
		<title>Quotients</title>
		<link>http://www.e-pig.org/epilogue/?p=319</link>
		<comments>http://www.e-pig.org/epilogue/?p=319#comments</comments>
		<pubDate>Mon, 08 Feb 2010 14:02:54 +0000</pubDate>
		<dc:creator>Conor</dc:creator>
				<category><![CDATA[General]]></category>
		<category><![CDATA[Observational Type Theory]]></category>

		<guid isPermaLink="false">http://www.e-pig.org/epilogue/?p=319</guid>
		<description><![CDATA[I&#8217;ve had an enquiry for more details on quotients in the new Epigram setup, so I&#8217;ll take that as a cue to blog a bit.
First, I&#8217;d better sketch some basics about propositions and equality. It&#8217;s the novel treatment of these things which lets us handle quotients in (hopefully) a neater way than has been possible [...]]]></description>
		<wfw:commentRss>http://www.e-pig.org/epilogue/?feed=rss2&amp;p=319</wfw:commentRss>
		<slash:comments>1</slash:comments>
		</item>
		<item>
		<title>EE-PigWeek 4-9 Jan 2010</title>
		<link>http://www.e-pig.org/epilogue/?p=306</link>
		<comments>http://www.e-pig.org/epilogue/?p=306#comments</comments>
		<pubDate>Wed, 13 Jan 2010 13:40:42 +0000</pubDate>
		<dc:creator>Conor</dc:creator>
				<category><![CDATA[General]]></category>

		<guid isPermaLink="false">http://www.e-pig.org/epilogue/?p=306</guid>
		<description><![CDATA[A big thanks to James Chapman for organising EE-PigWeek at the Institute of Cybernetics, Tallinn, Estonia. This time around, the crew comprised Brady, Chapman, Dagand, Gundry, McBride, Morris, and Norell. We started the week with an experimental system which did almost nothing. We finished the week with an experimental system which almost does something.
I&#8217;ll go [...]]]></description>
		<wfw:commentRss>http://www.e-pig.org/epilogue/?feed=rss2&amp;p=306</wfw:commentRss>
		<slash:comments>0</slash:comments>
		</item>
	</channel>
</rss>
