[TYPES] Types for Open Terms ?

[Adam Poswolsky]

Wow.  I'm also glad to see a renewed interest in open terms!

I would like to point out my work with Carsten Schuermann on the
Delphin Project where we created a dependently-typed languages which
supports HOAS.

Please see the website here:  http://cs-www.cs.yale.edu/homes/delphin/.

You can download the system.  The latest version is 1.5.1 and it is a
full release so everything is implemented including the coverage and
termination checker so the system will tell you if any cases are
missing or if the program may not terminate.

My dissertation explains the entire system starting with a
simply-typed version to gently explain the novelty in how we represent
open terms.

http://www.cs.yale.edu/homes/poswolsk/papers/poswolsky-dissertation.pdf

For a quick read, I suggest

Adam Poswolsky and Carsten Schürmann.  Practical Programming with
Higher-Order Encodings and Dependent Types.  In European Symposium on
Programming (ESOP 2008)

http://www.cs.yale.edu/homes/poswolsk/papers/delphinESOP08.pdf

The main novelty of our work in compared with the context-based
approaches are that just as in HOAS the context remains implicit, we
keep the context implicit and allow the user to reason over open terms
by just keeping track of the relative differences in the context.  In
particular, the type Nabla(x).Nabla(y).T represents a type T where
both x and y occur free.


If you are interested and have any other questions please don't hesitate to ask.

Cheers,

Adam

On Sat, Oct 15, 2011 at 1:17 PM, Brigitte Pientka <bpientka at cs.mcgill.ca> wrote:
> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
>
> Dear Jacques,
>
>  thank you for your interest in open terms and types!
>
> You may want to take a look at our work on Beluga which allows users
> to program with open terms. It may give you a more accessible way for
> playing with and understanding contextual objects.
>
> A Prototype for download is available at  http://complogic.cs.mcgill.ca/beluga/
>
> [Pientka 2008] A type-theoretic foundation for programming with
> higher-order abstract syntax and first-class substitutions, Brigitte
> Pientka, 35th Annual ACM SIGPLAN-SIGACT Symposium on Principles of
> Programming Languages (POPL'08), pages 371-382, ACM Press, 2008.
>
> [Cave, Pientka 2012] Programming with Binders and Indexed Data-types,
> Andrew Cave and Brigitte Pientka, accepted at 39th ACM SIGPLAN-SIGACT
> Symposium on Principles of Programming Languages (POPL'12)
>
> For gentle introductions:
>
> Beluga: programming with dependent types, contextual data, and
> contexts,Brigitte Pientka, Invited talk at 10th International
> Symposium on Functional and Logic Programming (FLOPS'10), April 2010,
> Sendai, Japan.
>
> Programming inductive proofs: a new approach based on contextual
> types, Brigitte Pientka, Verification, Induction, and Termination
> analysis, LNAI, Springer, Aug 2010
>
>
> Best wishes,
>
> - Brigitte
>
>
> On Thu, Oct 13, 2011 at 11:23 AM, Jacques Carette <carette at mcmaster.ca> wrote:
>> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
>>
>> I have been looking to find relevant work on types for open terms, i.e.
>> types for terms with free variables which are *not* in an environment.
>>
>> I have been able to find some work by Westbrook [1], Geuvers and Jojgov [2],
>> Geuvers, Krebbers, McKinna and Wiedijk [3] directly on this, as well as
>> depply inside Sacerdoti Coen's thesis [4].  It appears that and Nanevski,
>> Pfenning and Pientka [5]'s contextual modal type theory is "related" (but
>> scary in its complexity...), as compared say with Rhiger's much simpler
>> system [6] which seems to offer similar benefits as far as my needs go.
>>
>> What have I missed?
>>
>> Jacques
>>
>> [1] http://www.divms.uiowa.edu/~astump/papers/tfp06-free-var-types.pdf
>> [2] http://www.cs.ru.nl/~herman/PUBS/openlogic.pdf
>> [3] http://arxiv.org/abs/1009.2792v1
>> [4] http://www.cs.unibo.it/~sacerdot/tesidott/thesis.ps.gz
>> [5] http://dl.acm.org/citation.cfm?id=1352591
>> [6] http://akira.ruc.dk/~mir/Reports/tfp05-revised.pdf
>>
>>
>