Cayenne -- a language with dependent types

DOI10.1145/289423.289451MaRDI QIDQ5348900zbMATH OpenOpenAlexFDO

Authors 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 typeslanguage designmodule systemstype systems

Mathematics Subject Classification ID

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

Recommendations

• Cayenne -- a language with dependent types
• Dependently typed programming in Agda
• scientific article; zbMATH DE number 2090721
• Dependently typed records in type theory
• Dependent Types at Work

Cited in

(13)

• Adapting functional programs to higher order logic
• Constructive membership predicates as index types
• Language-based program verification via expressive types
• Imperative LF meta-programming
• Program calculation in Coq
• Unified syntax with iso-types
• Hoare type theory, polymorphism and separation
• Algebra of programming in Agda: Dependent types for relational program derivation
• A partial type checking algorithm for Type:Type
• Cayenne -- a language with dependent types
• A type system for reflective program generators
• Introducing VAUCANSON
• Dependently typed array programs don't go wrong

Describes a project that uses

Uses Software

• Cayenne

This page was built for publication: Cayenne -- a language with dependent types

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