|
|
|
|
|
|
by tel
3743 days ago
|
|
|
Without commenting on LambdaConf's statement, PrlConf refers to the JonPrl language but much, much more broadly the general PRL ("Proof Refinement Logic") system of proof languages of which Cornell's NuPRL (http://nuprl.org/) is by far the most advanced example. Unfortunately, NuPRL is engineered such that it is really difficult to get started with it and usually depends upon having access to an instance of a NuPRL server running at a major institution. This prevents the spread of the ideas of PRL and both JonPrl and PrlConf are, most likely, attempts to reverse that. Generally, PRL is a mechanism for proofs which varies slightly but significantly from the "proof calculus"-oriented provers like Coq/Agda by including at its very core an unbounded notion of untyped computation. This allows more interesting, exotic things to be expressed in PRL even if the proofs about them must ultimately be finite. |
|
|
One clarification—we called it PrlConf intending to talk about proof assistants, but as our program came together, it turned out that most of the talks were about category theory, type theory and denotational semantics. I think these things are even more interesting than proof assistants!
I hope that we can find a way to put it back on somehow.