So cancelling whatever Prl is seems like yet more internet outrage culture that we would be better off with less of.
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.