BEGIN:VCALENDAR VERSION:2.0 PRODID:ILLC Website X-WR-TIMEZONE:Europe/Amsterdam BEGIN:VTIMEZONE TZID:Europe/Amsterdam X-LIC-LOCATION:Europe/Amsterdam BEGIN:DAYLIGHT TZOFFSETFROM:+0100 TZOFFSETTO:+0200 TZNAME:CEST DTSTART:19700329T020000 RRULE:FREQ=YEARLY;BYMONTH=3;BYDAY=-1SU END:DAYLIGHT BEGIN:STANDARD TZOFFSETFROM:+0200 TZOFFSETTO:+0100 TZNAME:CET DTSTART:19701025T030000 RRULE:FREQ=YEARLY;BYMONTH=10;BYDAY=-1SU END:STANDARD END:VTIMEZONE BEGIN:VEVENT UID:/NewsandEvents/Archives/2022/newsitem/13863/7- September-2022-First-Workshop-on-Proofs-Computatio n-Meaning-Infinity-and-co-inductive-proofs DTSTAMP:20220908T150100 SUMMARY:First Workshop on Proofs, Computation & Me aning: Infinity and co-inductive proofs DTSTART;TZID=Europe/Amsterdam:20220907T100000 DTEND;TZID=Europe/Amsterdam:20220907T130000 DESCRIPTION:Around thirty years after the fall of Hilbert's program, the proofs-as-programs paradigm established the view that a proof should not be i dentified, as in Hilbert's metamathematics, with a string of symbols in some formal system. Rather, proofs should consist in computational or epistemi c objects conveying evidence to mathematical propo sitions. The relationship between formal derivatio ns and proofs should then be analogous to the one between words and their meanings. This view natura lly gives rise to questions such as “which conditi ons should a formal arrangement of symbols satisfy to represent a proof?” or “when do two formal der ivations represent the same proof?". These questio ns underlie past and current research in proof the ory both in the theoretical computer science commu nity (e.g. categorical logic, domain theory, linea r logic) and in the philosophy community (e.g. pro of-theoretic semantics). In spite of these common motivations and historical roots, it seems that t oday proof theorists in philosophy and in computer science are losing sight of each other. This work shop aims at contributing to a renaissance of the interaction between researchers with different bac kgrounds by establishing a constructive environmen t for exchanging views, problems and results. The workshop series includes three events, each focus ing on one specific aspect of proofs and their rep resentation. To foster interaction and discussion, each event will consists in short talks followed by a 15 minutes slot during which participants can engage in discussion or just take a short break. The first workshop focuses on Infinity and co-indu ctive proofs. X-ALT-DESC;FMTTYPE=text/html:\n
Around thirty years after the fall of Hilbert's program, the pro ofs-as-programs paradigm established the view that a proof should not be identified, as in Hilbert's metamathematics, with a string of symbols in some formal system. Rather, proofs should consist in c omputational or epistemic objects conveying eviden ce to mathematical propositions. The relationship between formal derivations and proofs should then be analogous to the one between words and their me anings. This view naturally gives rise to question s such as “which conditions should a formal arrang ement of symbols satisfy to represent a proof?” or “when do two formal derivations represent the sam e proof?". These questions underlie past and current research in proof theory both in the theor etical computer science community (e.g. categorica l logic, domain theory, linear logic) and in the p hilosophy community (e.g. proof-theoretic semantic s).
\nIn spite of these common motivations and historical roots, it seems that today proof t heorists in philosophy and in computer science are losing sight of each other. This workshop aims at contributing to a renaissance of the interaction between researchers with different backgrounds by establishing a constructive environment for exchan ging views, problems and results.
\nThe wo rkshop series includes three events, each focusing on one specific aspect of proofs and their repres entation. To foster interaction and discussion, ea ch event will consists in short talks followed by a 15 minutes slot during which participants can en gage in discussion or just take a short break. The first workshop focuses on Infinity and co-inducti ve proofs.
URL:http://ls.informatik.uni-tuebingen.de/pcm-onli ne/ CONTACT:luca.tranchini at gmail.com CONTACT:paolo.pistone at uniroma3.it END:VEVENT END:VCALENDAR