Cayenne
Cayenne — a language with dependent types. Cayenne is a Haskell-like language. The main difference between Haskell and Cayenne is that Cayenne has dependent types, i.e., the result type of a function may depend on the argument value, and types of record components (which can be types or values) may depend on other components. Cayenne also combines the syntactic categories for value expressions and type expressions; thus reducing the number of language concepts. Having dependent types and combined type and value expressions makes the language very powerful. It is powerful enough that a special module concept is unnecessary; ordinary records suffice. It is also powerful enough to encode predicate logic at the type level, allowing types to be used as specifications of programs. However, this power comes at a cost: type checking of Cayenne is undecidable. While this may appear to be a steep price to pay, it seems to work well in practice.
Keywords for this software
References in zbMATH (referenced in 25 articles )
Showing results 1 to 20 of 25.
Sorted by year (- Kahl, Wolfram: A mechanised abstract formalisation of concept lattices (2014)
- Abel, Andreas; Scherer, Gabriel: On irrelevance and algorithmic equality in predicative type theory (2012)
- Strub, Pierre-Yves; Swamy, Nikhil; Fournet, Cedric; Chen, Juan: Self-certification: bootstrapping certified typecheckers in F$^\ast$ with Coq (2012)
- Weirich, Stephanie; Casinghino, Chris: Generic programming with dependent types (2012)
- Abel, Andreas; Altenkirch, Thorsten: A partial type checking algorithm for type: type (2011)
- Abel, Andreas; Altenkirch, Thorsten: A partial type checking algorithm for Type:Type (2011)
- Lutteroth, Christof; Draheim, Dirk; Weber, Gerald: A type system for reflective program generators (2011)
- Wilson, Sean; Fleuriot, Jacques; Smaill, Alan: Automation for dependently typed functional programming (2010)
- Mu, Shin-Cheng; Ko, Hsiang-Shang; Jansson, Patrik: Algebra of programming in Agda: dependent types for relational program derivation (2009)
- Trojahner, Kai; Grelck, Clemens: Dependently typed array programs don’t go wrong (2009)
- Jia, Limin; Vaughan, Jeffrey A.; Mazurak, Karl; Zhao, Jianzhou; Zarko, Luke; Schorr, Joseph; Zdancewic, Steve: AURA: a programming language for authorization and audit (2008)
- Owens, Scott; Slind, Konrad: Adapting functional programs to higher order logic (2008)
- Stump, Aaron: Imperative LF meta-programming. (2008)
- Caldwell, James; Pohl, Josef: Constructive membership predicates as index types. (2007)
- Haiyan, Qiao: Testing and proving distributed algorithms in constructive type theory (2007)
- Sheard, Tim: Type-level computation using narrowing in omegamega. (2007)
- Stump, Aaron: Imperative LF meta-programming (2007)
- Sulzmann, Martin; Voicu, Razvan: Language-based program verification via expressive types. (2007)
- Xi, Hongwei: Dependent ML an approach to practical programming with dependent types (2007)
- Brady, Edwin; Hammond, Kevin: A dependently typed framework for static analysis of program execution costs (2006)