-*- coding: utf-8; indent-tabs-mode: nil; -*-

This document describes the Beluga source code, including a
description of the source code structure and a description of the
Beluga project.

*      [Version History]
*      [Structure]
*      [Project Description]
       *        [Contextual Modal Type Theory]


Version History
===============

    0.1-20090925        First public release of Beluga

    0.1-20091016        First version to compile under OCaml 3.11 (as well as 3.10)

    0.1-20091215        Support for context subsumption

    0.2-20100122        `interpreter' now typechecks _and interprets_ Beluga code;
                        improved error messages; improved Unicode support



Structure
=========


beluga
------

    INSTALL             Compilation and installation instructions
    README              Current file
    STYLE               Comments on stylistic conventions
    TODO                List of tasks to be completed


src
---
  OMakefile
  

src/core:
---------
    abstract.ml         Abstraction
    abstract.mli
    check.ml            Typechecking
    check.mli           
    common.ml
    common.mli
    config.ml           State configuration for Core
    context.ml          Contexts 
    context.mli         
    ctxsub.ml           Context substitutions
    ctxsub.mli          
    cwhnf.ml            Contextual Weak head normalization
    cwhnf.mli
    debug.ml            Debugging flags
    error.ml
    error.mli           Error handling
 
    gensym.ml           Unique symbol generation
    gensym.mli          
    id.ml               Identifiers, used for variables, constants, etc.
    id.mli               
    lexer.ml            Lexer
    lexer.mli  
    monitor.ml          Timing 
    monitor.mli
    parser.ml           Parser
    parser.mli
    pretty.ml           Pretty printing
    pretty.mli 
    reconstruct.ml      Type reconstruction for LF and computations
    reconstruct.mli
    store.ml            Variable store, maps ids to variable information
    store.mli           
    substitution.ml     Explicit substitution operations (ordinary and contextual)
    substitution.mli
    syntax.ml           Syntax for the LF and computation layer of Beluga
    syntax.mli
    token.ml            Tokens for parsing
    trail.ml            Trailing meta-variables for backtracking
    trail.mli
    unify.ml            Higher-order unification
    whnf.ml             Weak-head normalization
    whnf.mli        



src/main
-----------

   OMakefile
   main.ml              Main top level


tools
-----
  beluga-mode.el        Emacs mode for Beluga programs


Project Description
===================


  Our main interest in this project is to investigate programming 
and reasoning with data structures that provide support for binders. 
Many object languages include binding constructs, and it is striking 
that functional languages still lack direct support for binders and 
common tricky operations such as renaming, capture-avoiding substitution,
 and fresh name generation.

We advocate the use of higher-order abstract syntax (HOAS) where we 
represent binders in the object language with binders in the meta-language. 
One of the key benefits is that we not only get support for renaming 
and fresh name generation, but also for capture-avoiding substitution. 
While HOAS encodings have played an important role in mechanizing the 
meta-theory of programming languages, it has been difficult to incorporate 
HOAS encodings directly into functional programming. 

The Beluga implementation provides an implementation of the logical
framework LF, and in addition a functional programming environment
which supports dependent types and analyzing LF data via pattern 
matching. It is a completely new implementation effort. Its
implementation of the logical framework LF in OCaml shares, adapts and 
extends some fundamental ideas from the Twelf system. The functional
programming environment which is built on top of the logical framework
LF is a completely new implementation based on previous theoretical
ideas presented in [Pientka:POPL08] and [PientkaDunfield:PPDP08]. 


Publications
============

  * Brigitte Pientka and Joshua Dunfield. 
    Programming with proofs and explicit contexts. 
    In ACM SIGPLAN Symposium on Principles and Practice of Declarative 
    Programming (PPDP'08), pages 163-173. ACM Press, July 2008. 

  * Joshua Dunfield and Brigitte Pientka. 
    Case analysis of higher-order data. 
    In International Workshop on Logical Frameworks and Meta-Languages: 
    Theory and Practice (LFMTP'08). Elsevier, June 2008.

  * Brigitte Pientka. 
    A type-theoretic foundation for programming with higher-order abstract 
    syntax and first-class substitutions. 
    In 35th ACM Symposium on Principles of Programming Languages (POPL'08), 
    pages 371-382. ACM Press, January 2008. 

