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&nbsp\;\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