Skip to content
This repository has been archived by the owner on Feb 18, 2020. It is now read-only.

Latest commit

 

History

History
134 lines (131 loc) · 5.24 KB

readme.md

File metadata and controls

134 lines (131 loc) · 5.24 KB
Raw

Proof Carrying Code for MiniML

The idea is to create PCC framework for MiniML - subset of OCaml Light language.

Current status

Implementing MiniML compiler to ZINC bytecode

Currently working on

  • Defunctionalization of MiniML evaluator
  • Defunctionalization of Enriched Lambda Calculus evaluator
  • Description of MiniML
  • Description of Enriched Lambda Calculus

Changelog

  • 26 XI 2012
    • [Languages]
      • Correct definition of Values for MiniML
      • Rewrote typing for MiniML
      • Rewrote evaluation for MiniML
      • Parsing funtion applications without @ operator in MiniML
      • Parsing funtion applications without @ operator in EnrichedLambda Calculus
    • [Utils]
      • Slightly modified Language class (program can have not Type & no Value)
      • Interpreter can now show defined bindings
      • Added help text to the interpreter
  • 23 XI 2012
    • [Languages]
      • Finished work on Enriched Lambda Calculus
    • [Bug Fixes]
      • Fixed bug in Enriched Lambda Calculus function parser
      • Correct typing in case clauses in Enriched Lambda Calculus
      • Correct typing of constructors in Enriched Lambda Calculus
      • Unification in proper places to have polymorphism
    • [Utils]
      • Added functional dependencies and new language name parameter to Language
      • Added free variables counter parameter to typing functions in language class
      • Very basic version of generic interpreter
  • 14 XI 2012
    • [Languages]
      • Parser for Enriched Lambda Calculus
      • Laguage class instance declaration for Enriched Lambda Calculus
  • 13 XI 2012
    • [Languages]
      • Values as memory cells in Enriched Lambda Calculus
      • Evaluator for Enriched Lambda Calculus
      • Returned to simple definition form im Enriched Lambda Calculus
    • [Utils]
      • Cleaning and restructuring typeclasses
      • Distinguishing evaluation environment from typing environment
  • 5 XI 2012
    • [Languages]
      • Added Value type to Enriched Lambda Calculus
      • Typing of enriched Enriched Lambda Calculus
  • 4 XI 2012
    • [Languages]
      • Added (internal) guards on patterns in MiniML
      • Made case statements internal in MiniML
      • LetRec in MiniML are now less restrictive and are allowing expressions on right hand side (previously only functions were allowed)
      • Added rescue expression to EnrichedLambda (it behaves like FatBar in MiniML)
    • [Compiler]
      • Translating patterns with constants to guarded patterns
      • Transforming let and letrec definitions to declarations (with only variable patterns allowed)
      • Pattern Matchings translated to FatBars and PatternMatching labdas according to [PJ87]
      • Compilation of pattern matching finished
      • Translation to enriched lambda calculus finished
  • 29 X 2012
    • [Languages]
      • Moved prety printing utility functions to PrettyPrint modules from Syntax
  • 22 X 2012
    • [Languages]
      • Removed old Enriched Lambda Calculus Code
    • [Compiler]
      • Removing redundant if stateents introduced by pattern matching simplification
      • Added translation to Enriched Lambda Calculus
  • 21 X 2012
    • [Languages]
      • Added head, tail, empty?, fst and snd primitives to MiniML
    • [Compiler]
      • Initial version of pattern matching translations
  • 10 IX 2012
    • [Compiler]
      • Changed compiler structure
      • Added folding tuples
      • Added wildcard pattern removing
  • 9 IX 2012
    • [Languages]
      • Deleted Enriched Lambda Calculus With Low Level Types
      • Rewrote Enriched Lambda Calculus syntax to be similar to Core language described in Implementing Functional Languages: a tutorial
  • 18 VIII 2012
    • [Languages]
      • MiniML interpreter reimplemented using monads
      • Mutually recursive letrec in Enriched Lambda Calculus With Low Level Types
      • Added definitions to Enriched Lambda Calculus With Low Level Types
    • [Compiler]
      • Finished transaltion from Enriched Lambda Calculus to Enriched Lambda Calculus With Low Level Types
    • [Others]
      • Enriched Lambda Calculus interpreter now uses record as sate
  • 15 VIII 2012
    • [Compiler]
      • Finished transaltion from MiniML to Enriched Lambda Calculus
  • 11 VIII 2012
    • [Languages]
      • Mutually recursive letrec in Enriched Lambda Calculus
    • [Compiler]
      • Enforcing unique variable naming
  • 7 VIII 2012
    • [Languages]
      • Added definitions to Enriched Lambda Calculus
  • 6 VIII 2012
    • [Others]
      • Cleanup, introducing git flow, readme creation
  • 10 VI 2012
    • [Languages]
      • Working version of Enriched Lambda Calculus With Low Level Types Interpreter
  • 7 VI 2012
    • [Compiler] *Translation from Enriched Lambda Calculus to Enriched Lambda Calculus With Low Level Types
  • 27 V 2012
    • [Compiler]
      • Translation from MiniML to Enriched Lambda Calculus
  • 4 V 2012
    • [Languages]
      • Working version of Enriched Lambda Calculus interpreter
  • 14 IV 2012
    • [Languages]
      • Working version of MiniML interpreter
  • 5 III 2012
    • [Others]
      • The project begins