University of Sussex
Browse

File(s) under permanent embargo

Monadic presentations of Lambda terms using generalized inductive types

chapter
posted on 2023-06-07, 14:13 authored by Thorsten Altenkirch, Bernhard ReusBernhard Reus
We present a definition of untyped l-terms using a heterogeneous datatype, i.e. an inductively defined operator. This operator can be extended to a Kleisli triple, which is a concise way to verify the substitution laws for l-calculus. We also observe that repetitions in the definition of the monad as well as in the proofs can be avoided by using well-founded recursion and induction instead of structural induction. We extend the construction to the simply typed l-calculus using dependent types, and show that this is an instance of a generalization of Kleisli triples. The proofs for the untyped case have been checked using the LEGO system.

History

Publication status

  • Published

Journal

CSL '99: Proceedings of the 13th International Workshop and 8th Annual Conference of the EACSL on Computer Science Logic

Publisher

Springer-Verlag

Volume

1863

Page range

453-468

Pages

580.0

Book title

Computer Science Logic: Proceedings of the 13th International Workshop CSL '99, 8th Annual Conference of the EACSL, Madrid, Spain

ISBN

9783540665366

Series

Lecture Notes in Computer Science

Department affiliated with

  • Informatics Publications

Full text available

  • No

Peer reviewed?

  • Yes

Editors

Mario Rodriguez-Artalejo, Jörg Flum

Legacy Posted Date

2008-03-03

Usage metrics

    University of Sussex (Publications)

    Categories

    No categories selected

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC