A dependent type is a type whose definition depends on a value.
Some common forms of dependent type are
- product types Π
- sum types Σ
- sized vector types such as “N-bit bitvectors”.
See also: Barendregt cube.
Notes related to Dependent type
Arm Architecture Specification Language (ASL), Coq theorem prover, Liquid type, Phantom types, Sail ISA specification language
Papers related to Dependent type
- Detailed models of instruction set architectures: From pseudocode to formal semantics [armstrong:arw:2018]
- ISA semantics for ARMv8-A, RISC-V, and CHERI-MIPS [armstrong:popl19:2019]
- The state of Sail [armstrong:spisa:2019]
- Dependent types for low-level programming [condit:esop:2007]
- Secure information flow verification with mutable dependent types [ferraiuolo:dac:2017]
- Checking type safety of foreign function calls [furr:pldi:2005]
- Faking it: Simulating dependent types in Haskell [mcbride:jfp:2002]
- Ynot: Dependent types for imperative programs [nanevski:icfp:2008]
- Specifying concurrent programs in separation logic: Morphisms and simulations [nanevski:oopsla:2019]
- End-to-end verification of ARM processors with ISA-formal [reid:cav:2016]
- Trustworthy specifications of ARM v8-A and v8-M system level architecture [reid:fmcad:2016]
- Who guards the guards? Formal validation of the ARM v8-M architecture specification [reid:oopsla:2017]
- Liquid types [rondon:pldi:2008]
- A dependently typed assembly language [xi:icfp:2001]
- Dependent ML An approach to practical programming with dependent types [xi:jfp:2007]