BEGIN:VCALENDAR
PRODID:-//eluceo/ical//2.0/EN
VERSION:2.0
CALSCALE:GREGORIAN
BEGIN:VEVENT
UID:www.tcs.tifr.res.in/event/234
DTSTAMP:20230914T125915Z
SUMMARY:A Logic of Interactive Proofs
DESCRIPTION:Speaker: Simon Kramer\nUniversity of Luxembourg\nInterdisciplin
ary Centre for\nSecurity and Trust Campus\nKirchberg\, F103 6\, rue\nRicha
rd Coudenhove-\nKalergi 1359 \;\nLuxembourg\n\nAbstract: \nWe propose
a logic of interactive proofs as the first and main step towards an intuit
ionistic foundation for interactive computation to be obtained via an inte
ractive analog of the Godel Kolmogorov-Artemov definition of intuitionisti
c logic as embedded into a classical modal logic of proofs\, and of the Cu
rry-Howard isomorphism between intuitionistic proofs and typed programs. O
ur interactive proofs effectuate a persistent epistemic impact in their in
tended communities of peer reviewers that consists in the induction of the
(propositional) knowledge of their proof goal by means of the (individual
) knowledge of the proof with the interpreting reviewer. That is\, interac
tive proofs effectuate a transfer of propositional knowledge -- (to-be-)kn
own facts -- via the transfer of certain individual knowledge -- (to-be-)k
nown proofs -- in multi-agent systems. In other words\, we as a community
have the formal common knowledge that a proof is that which if known to on
e of our peer members would induce the knowledge of its proof goal with th
at member.\n
URL:https://www.tcs.tifr.res.in/web/events/234
DTSTART;TZID=Asia/Kolkata:20111219T113000
DTEND;TZID=Asia/Kolkata:20111219T123000
LOCATION:AG-80
END:VEVENT
END:VCALENDAR