FPU talk Thursday 4 November, 1-2pm, ICT Building
3 views
Skip to first unread message
bjpop
Oct 26, 2010, 8:26:56 PM10/26/10
to fpunion
(Note the unusual time and place - this talk is also a Postgrad
seminar).
Title: Typed λ-calculus with constructors: A case study in mechanized
metatheory.
Speaker: Ben Horsfall.
Abstract:
This talk is the sequel to an earlier FPU talk that proposed a type
system for the λ-calculus with constructors (λBC) of Arbiser, Miquel &
Ríos (JFP 2009), which they acknowledge to "deeply challenge the
traditional intuition of the notion of type". My first FPU system was
incorrect, and unnecessarily elaborate. I now present what I believe
to be a correct type system (and compare it with Petit's similar
proposal (TLCA 2009) which uses intersection types to describe
subtyping). But the focus will be on my experiences trying to
mechanically formalize the type system using various proof assistants
and approaches, and my current results: in particular using Coq +
metalib; Twelf, which naturally supports the method of higher-order
abstract syntax (HOAS); and most recently and successfully Coq +
Chlipala's (ICFP 2008) method of parametric higher-order abstract
syntax (PHOAS). Twelf -- which is a sort of dependently-typed Prolog
with mode and coverage checking -- appeared very promising up until
contact which its coverage system and its worlds system (which manages
host-language type contexts, and introduces annoying backwards
dependencies). The interaction of these two is perplexing to say the
least. Coq and Agda do not support the standard HOAS method. Those
systems require that inductive type definitions be strictly positive,
to ensure termination of proofs. The guiding problem for the three
approaches is how to do the bookkeeping for binding variables, and I
believe that *HOAS approaches -- which represent variable abstractions
using abstractions in the host language -- are the best available (vs.
metalib, nominal logic, de Bruijn, etc.) But it turns out that this is
the least of our difficulties with λBC.
We hope to see you there.
seminar).
Title: Typed λ-calculus with constructors: A case study in mechanized
metatheory.
Speaker: Ben Horsfall.
Abstract:
This talk is the sequel to an earlier FPU talk that proposed a type
system for the λ-calculus with constructors (λBC) of Arbiser, Miquel &
Ríos (JFP 2009), which they acknowledge to "deeply challenge the
traditional intuition of the notion of type". My first FPU system was
incorrect, and unnecessarily elaborate. I now present what I believe
to be a correct type system (and compare it with Petit's similar
proposal (TLCA 2009) which uses intersection types to describe
subtyping). But the focus will be on my experiences trying to
mechanically formalize the type system using various proof assistants
and approaches, and my current results: in particular using Coq +
metalib; Twelf, which naturally supports the method of higher-order
abstract syntax (HOAS); and most recently and successfully Coq +
Chlipala's (ICFP 2008) method of parametric higher-order abstract
syntax (PHOAS). Twelf -- which is a sort of dependently-typed Prolog
with mode and coverage checking -- appeared very promising up until
contact which its coverage system and its worlds system (which manages
host-language type contexts, and introduces annoying backwards
dependencies). The interaction of these two is perplexing to say the
least. Coq and Agda do not support the standard HOAS method. Those
systems require that inductive type definitions be strictly positive,
to ensure termination of proofs. The guiding problem for the three
approaches is how to do the bookkeeping for binding variables, and I
believe that *HOAS approaches -- which represent variable abstractions
using abstractions in the host language -- are the best available (vs.
metalib, nominal logic, de Bruijn, etc.) But it turns out that this is
the least of our difficulties with λBC.
We hope to see you there.
Bernie Pope
Oct 26, 2010, 8:28:53 PM10/26/10
to fpu...@googlegroups.com
I forgot to mention: the location is yet to be determined, and will be confirmed in a later email.
Cheers,
Bernie.
> --
> To unsubscribe from this group, send email to fpunion-u...@googlegroups.com
Bernie Pope
Oct 29, 2010, 1:49:56 AM10/29/10
to fpu...@googlegroups.com
Due to a clash with a workshop we've had to move Ben's upcoming FPU talk to a different day and time.
The new details are:
When: Monday 8 Nov, 11am - 12 noon.
Where: 4.04, ICT Building, The University of Melbourne (111 Barry St, Carlton).
Cheers,
Bernie.
Reply all
Reply to author
Forward
0 new messages