BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY: Generic bidirectional typing for dependent type theories - Thiago
  Felicissimo\, INRIA
DTSTART:20231003T100000Z
DTEND:20231003T110000Z
UID:TALK205852@talks.cam.ac.uk
CONTACT:47138
DESCRIPTION:Algebraic/logical framework presentations of dependent type th
 eories suffer from the verbosity of the required type annotations\, which 
 destroys any hope of practical usability. In order to restore usability\, 
 standard presentations usually omit the majority of these annotations\, bu
 t this has a cost: because knowing them is still important when typing ter
 ms\, it becomes unclear how to do this algorithmically.\n\nA solution to t
 his problem is provided by bidirectional typing\, in which the typing judg
 ment is decomposed explicitly into inference and checking modes\, allowing
  to control the flow of type information in typing rules and to specify al
 gorithmically how the rules should be used. Bidirectional typing has been 
 fruitfully studied and bidirectional systems have been developed for many 
 type theories. However\, the formal development of bidirectional typing ha
 s until now been kept confined to specific theories\, with general guideli
 nes remaining informal.\n\nThe goal of this work is to give a generic acco
 unt of bidirectional typing for a wide class of dependent type theories. F
 or this\, we start by giving a general definition of type theories (or equ
 ivalently\, a logical framework)\, which differs from previous frameworks 
 by allowing for the usual unannotated syntaxes most often used in practice
 . Each theory then gives rise to a declarative and a bidirectional typing 
 system\, the latter being defined only for the inferable and checkable ter
 ms (for non-degenerate theories\, these coincide respectively with neutral
 s and normal forms). We then show\, in a theory-independent fashion\, that
  the two systems are equivalent. This equivalence is then explored to esta
 blish\, for weak normalizing theories\, the decidability of inference for 
 inferable terms\, and the decidability of checking for checkable terms.\n\
 n\n
LOCATION:FW26\, Computer Laboratory
END:VEVENT
END:VCALENDAR