/Agda-LLS

An Implementation of Various Linear Logics in Agda

Primary LanguageHaskellBSD 3-Clause "New" or "Revised" LicenseBSD-3-Clause

An Implementation of Various Linear Logics in Agda (ALL)

Design

The design of ALL is based the following:

  • Haskell Frontend:
    • Repl:
      • Haskeline
  • Agda Backend:
    • Parsers (written in combined Agda/Haskell):
      • Alex
      • Parsec
    • Type Checker
    • Evaluator
    • Formal verification:
      • Dialectica categories
      • Petri nets
    • Pretty Printer

The Agda backend will be a "server" that will take in various command-line options and a linear-logic expression that will then be parsed by a combined Agda/Haskell parser. The parser will turn the input expression into an intermediate representation -- without locally-nameless -- that will be shared between both Haskell and Agda using the FFI, but then will be translated into locally-nameless representation on the Agda side.