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 29 articles )
Showing results 1 to 20 of 29.
Sorted by year (- Stump, Aaron: The calculus of dependent lambda eliminations (2017)
- Yang, Yanpeng; Bi, Xuan; Oliveira, Bruno C.d. S.: Unified syntax with iso-types (2016)
- Kahl, Wolfram: A mechanised abstract formalisation of concept lattices (2014)
- Swamy, Nikhil; Chen, Juan; Fournet, Cédric; Strub, Pierre-Yves; Bhargavan, Karthikeyan; Yang, Jean: Secure distributed programming with value-dependent types (2013)
- 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)
- Lutteroth, Christof; Draheim, Dirk; Weber, Gerald: A type system for reflective program generators (2011)
- Tesson, Julien; Hashimoto, Hideki; Hu, Zhenjiang; Loulergue, Frédéric; Takeichi, Masato: Program calculation in Coq (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)
- 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 (\Omega)mega (2007)
- Stump, Aaron: Imperative LF meta-programming (2007)
- Sulzmann, Martin; Voicu, Rǎzvan: Language-based program verification via expressive types (2007)