Cayenne—a language with dependent types

DOI10.1145/289423.289451zbMath1369.68085OpenAlexW2027584005MaRDI QIDQ5348900

Lennart Augustsson

Publication date: 21 August 2017

Published in: Proceedings of the third ACM SIGPLAN international conference on Functional programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1145/289423.289451

zbMATH Keywords

dependent typestype systemsmodule systemslanguage design

Mathematics Subject Classification ID

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

Related Items

Dependently typed array programs don't go wrong, Unified Syntax with Iso-types, Hoare type theory, polymorphism and separation, A Partial Type Checking Algorithm for Type:Type, A type system for reflective program generators, Introducing VAUCANSON, Program Calculation in Coq, Algebra of programming in Agda: Dependent types for relational program derivation, Adapting functional programs to higher order logic, Constructive Membership Predicates as Index Types, Language-Based Program Verification via Expressive Types, Imperative LF Meta-Programming

Uses Software

• Cayenne