Code for the paper:

  Refinement types and computational duality
  http://www.cs.cmu.edu/~noam/papers/rtcd.pdf

Copyright (c) 2008, Noam Zeilberger

Overview of files (compiled with Agda 2.1.3):

  (main files)
  BaseI.agda	  intrinsic syntax/semantics (deep patterns, higher-order)
  RefineI.agda	  extrinsic refinements (deep patterns, higher-order)
  BaseF.agda	  intrinsic syntax (shallow patterns, defunctionalized)
  RefineF.agda	  extrinsic refinements (shallow patterns, defunctionalized)

  (useful libraries)
  Index.agda	  de Bruijn indices
  Split.agda	  context splittings
  SumsProds.agda  sums/products
  ListFacts.agda  some list routines and lemmas

Last updated: October 2008.
