/[mojave]/metaprl/theories/mc/README
ViewVC logotype

Diff of /metaprl/theories/mc/README

Parent Directory Parent Directory | Revision Log Revision Log | View Patch Patch

revision 3582 by emre, Fri Apr 5 07:07:58 2002 UTC revision 3583 by emre, Thu Apr 25 05:26:29 2002 UTC
# Line 1  Line 1 
1  Maintainer of this theory: Brian Emre Aydemir (emre@its.caltech.edu)  Maintainer of this theory: Brian Emre Aydemir (emre (a) its.caltech.edu)
2  Last update to this file: 4 April 2002  Last update to this file: 24 April 2002
3    
 THIS FILE IS REALLY INCOMPLETE!  
4    
5  I describe the purpose of this theory and its implementation in this file.  <<
6       Pending issues concerning this file:
7       -  At some point, the Caltech PRL group will have a webpage, so
8          I can actually include the website for MC in here.
9    >>
10    
11    
12  Overview:  Overview:
13  --------------------------------------------------------------------------  --------------------------------------------------------------------------
14  The purpose of this theory is to provide a formal representation of the  The Mojave Compiler (MC) is one component of the Caltech PRL group's mission to
15  Mojave compiler's FIR.  develop methods and tools for building safe and reliable distributed systems.
16    At it's core, MC uses a typed, mostly functional intermediate representation
17  << more information should go here eventually >>  (FIR).  Every source language compiled by MC is eventually transformed into the
18    FIR language.  By combining MC with a theorem prover / logical programming
19    environment, e.g. MetaPRL, it is believed that we will be able to reason about
20    code and perform higher level optimizations and program transformations that
21    typical compilers are unable to perform.  The goal of this theory is to
22    formalize the FIR in order to perform these transformations and to reason about
23    FIR programs.
24    
25    Currently, there are terms for everything in the FIR, some minimal operational
26    semantics, and partial implementations of some trivial optimizations.  The
27    truly "interesting" portions of this theory will be investigated and
28    implemented this summer, hopefully.  (My classes severely limit the amount of
29    time I can devote to working on this theory during the academic school year.)
30    
31    On a related note, Adam Granicz (granicz (a) cs.caltech.edu) is currently
32    working on using the MetaPRL term rewriting system to transform source files in
33    MC into the FIR terms defined here.
34    
35    
36  Compilation issues:  Compilation issues:
37  --------------------------------------------------------------------------  --------------------------------------------------------------------------
38  While this theory is intended to compile with (as in, be linked with)  While this theory is intended to compile with (as in, be linked with) the
39  the Mojave compiler, though it will compile without as well.  In order  Mojave Compiler, it will compile without it as well. In order to compile
40  to compile with MC, you must set the MC_ROOT environment variable to point to  MetaPRL and MC together, you will need to:
 the the root directory of MC.  
41    
42    1) cons must be used to build MetaPRL if MC support is to be included.
43       cons can be obtained at http://www.dsmit.com/cons/
44    
45  Module -- Mp_mc_term_op:  2) Set the MC_ROOT environment variable to point to the root directory
46  --------------------------------------------------------------------------     of the MC source tree.
47  This module provides basic term construction and deconstruction operations  
48  similar to those in Refiner.Refiner.TermOp.  The most notable difference is my  3) Run cons from the root directory of the MetaPRL source tree.
 naming scheme for the functions.  This scheme and other information is  
 documented in mp_mc_term_op.mli.  

Legend:
Removed from v.3582  
changed lines
  Added in v.3583

  ViewVC Help
Powered by ViewVC 1.1.26