A simple type-theoretic language: Mini-TT

MaRDI QIDQ3400627zbMATH OpenFDO

Authors Thierry Coquand, Yoshiki Kinoshita, Bengt Nordström, Makoto Takeyama

Publication date 5 February 2010

zbMATH Keywords

small functional language with dependent types

Mathematics Subject Classification ID

Theory of programming languages (68N15) Functional programming and lambda calculus (68N18)

Recommendations

• A tutorial implementation of a dependently typed lambda calculus
• A Brief Overview of Agda – A Functional Language with Dependent Types
• Idris, a general-purpose dependently typed programming language: Design and implementation
• Derivation of a parsing algorithm in Martin-Löf's theory of types
• Dependent ML An approach to practical programming with dependent types

Cited in

(3)

• PICCOLA -- a small composition language
• A tutorial implementation of a dependently typed lambda calculus
• Dependent Types at Work

Describes a project that uses

Uses Software

• Haskell

This page was built for publication: A simple type-theoretic language: Mini-TT

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3400627)