Positive inductive-recursive definitions

• Agda development:
  • Clickable HTML.
  • Plain .agda files: positive.tar.gz.
• Paper: positive.pdf. Also available at the LMCS website.

Update June 2017 for Agda development: Added introduction rules (bypassing Agda's checks for convenience), and worked out the details for the nested type Lam. Prompted by a question from Larry Diehl.

  @ARTICLE{GhaniMalatestaNordvallforsberg2015posIR,
     author    = {Ghani, Neil and Malatesta, Lorenzo and Nordvall Forsberg, Fredrik},
     title     = {Positive Inductive-Recursive Definitions},
     journal   = {Logical Methods in Computer Science},
     volume    = {11},
     number    = {1},
     year      = {2015},
     doi       = {10.2168/LMCS-11(1:13)2015},
  }