\n

\n The extraction of computational content from proofs has a long\n tradition in logic, but usually depends on a concrete encoding\n t hat allows us to turn proofs into algorithms. A re cent trend\n in this field is the departure from such encoding which not\n only makes it simpler to represent the mathematical content,\ n but also makes the extracted computationa l content encoding\n independent. This shif t in focus allows us to focus on what is\n relevant: the computational aspects of proofs and the\n specification (not representation) of the structures\n involved. We now have gro wing evidence that this move from\n represe ntations (e.g. the signed digit representation of the\n reals) to axioms (e.g. of the real nu mbers) is possible. This\n development larg ely parallels the step from assembler to high\n level languages in programming. As a by-produ ct this move has\n already opened up the po ssibility to gain computational\n informati on from axiomatic proofs in more abstract and\n genuinely structural areas of mathematics suc h as algebra and\n topology.\n

\n \n \nFor more information, see htt p://vsl2014.at/psc/\n or contact psc2014 at easych air.org.\n

\n\n <
p>We welcome 1-2-page abstracts presenting (finish
ed, ongoing, or if\n clearly stated even pu
blished) work on proof, structure, and computation
.\n Submission deadline is 1 May 2014.\n
\n

URL:/NewsandEvents/Archives/2014/newsitem/5693/17-
18-July-2014-International-Workshop-on-Proof-Struc
ture-and-Computation-PSC-2014-Vienna-Austria
END:VEVENT
END:VCALENDAR