BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//wp-events-plugin.com//7.2.3.1//EN
TZID:Europe/Paris
X-WR-TIMEZONE:Europe/Paris
BEGIN:VEVENT
UID:6989@i2m.univ-amu.fr
DTSTART;TZID=Europe/Paris:20190704T110000
DTEND;TZID=Europe/Paris:20190704T123000
DTSTAMP:20241120T202643Z
URL:https://www.i2m.univ-amu.fr/evenements/checking-correctness-for-recurs
 ive-definitions-with-mixed-inductive-and-coinductive-types/
SUMMARY:Pierre Hyvernat (LAMA\, Université Savoie Mont Blanc): Checking co
 rrectness for recursive definitions with mixed inductive and coinductive t
 ypes
DESCRIPTION:Pierre Hyvernat: The Size-Change Principle (SCP) is a simple al
 gorithm giving a partial termination test for recursive definitions. If th
 e language is lazy\, it also gives (by duality) a partial productivity tes
 t for recursive functions involving coinductive types. This is what is use
 d in Agda.\n\nUnfortunately\, when inductive and coinductive types are nes
 ted\, this is unsound: there are "well typed" and terminating recursive de
 finitions producing terms in empty types. Such definitions make Agda incon
 sistent.\n\nUsing ideas from L. Santocanale about circular proof and parit
 y games\, I'll show how the SCP can be used to check "totality" of recursi
 ve definitions. Besides the SCP\, the main ingredient is a more informativ
 e of notion call-graph\, and I'll sketch the proof of correctness by defin
 ing their "untyped" semantics using power domains.\n\n\n
ATTACH;FMTTYPE=image/jpeg:https://www.i2m.univ-amu.fr/wp-content/uploads/2
 020/01/Pierre_Hyvernat.jpg
CATEGORIES:Séminaire,Logique et Interactions
END:VEVENT
BEGIN:VTIMEZONE
TZID:Europe/Paris
X-LIC-LOCATION:Europe/Paris
BEGIN:DAYLIGHT
DTSTART:20190331T030000
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
TZNAME:CEST
END:DAYLIGHT
END:VTIMEZONE
END:VCALENDAR