[TYPES] Types for Open Terms ?

[Brigitte Pientka]

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
>
>