-
Views
-
Cite
Cite
Dirk Pattinson, Peter Schuster, Ana Sokolova, Preface for the special issue of Proof, Structure, and Computation 2014, Journal of Logic and Computation, Volume 29, Issue 4, 1 August 2019, Pages 417–418, https://doi.org/10.1093/logcom/exw007
Close - Share Icon Share
Extract
This special issue contains selected papers from the International Workshop on Proof, Structure, and Computation (PSC) held in Vienna on 17–18 July 2014, within the Vienna Summer of Logic (VSL). PSC was a CSL–LICS-affiliated workshop on the extraction of computational content from proofs.
The focus is on the computational aspects of proofs and the specification of the structures involved; the topics of interest are proof theory, program extraction, constructive mathematics, topology and computation, realizability semantics, coalgebra and computation, categorical models and domain theory.
The extraction of computational content from proofs has a long tradition in logic, but usually depends on a concrete encoding that allows us to turn proofs into algorithms. A recent trend in this field is the departure from such encoding, which not only makes it simpler to represent the mathematical content, but also makes the extracted computational content encoding independent. This shift in focus allows us to focus on what is relevant: the computational aspects of proofs and the specification (not representation) of the structures involved. We now have growing evidence that this move from representations (e.g. the signed-digit representation of the reals) to axioms (e.g. of the real numbers) is possible. This development largely parallels the step from assembler to high-level languages in programming. As a by-product, this move has already opened up the possibility to gain computational information from axiomatic proofs in more abstract and genuinely structural areas of mathematics such as algebra and topology.
