Dependently typed array programs don't go wrong

DOI10.1016/j.jlap.2009.03.002zbMath1187.68320OpenAlexW2569339511MaRDI QIDQ843222

Kai Trojahner, Clemens Grelck

Publication date: 29 September 2009

Published in: The Journal of Logic and Algebraic Programming (Search for Journal in Brave)

Full work available at URL: http://dare.uva.nl/personal/pure/en/publications/dependently-typed-array-programs-dont-go-wrong(f5e7edc3-30f6-4fc9-903a-b886513faf9a).html

zbMATH Keywords

dependent typesprogram verificationarray programming

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Theory of software (68N99)

Related Items (3)

Dependently typed array programs don't go wrong ⋮ Unnamed Item ⋮ APLicative Programming with Naperian Functors

Uses Software

• Matlab
• APL
• Cayenne

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Dependently typed array programs don't go wrong
• Indexed types
• SAC -- a functional array language for efficient multi-threaded execution
• Implementation and application of functional languages. 16th international workshop, IFL 2004, Lübeck, Germany, September 8--10, 2004. Revised selected papers.
• A Binding Scope Analysis for Generic Programs on Arrays
• The view from the left
• Cayenne—a language with dependent types
• An Approach to Fast Arrays in Haskell
• Polymorphism and separation in hoare type theory
• The Design of APL
• Shared memory multiprocessor support for functional array processing in SAC
• Types for Proofs and Programs
• Verification, Model Checking, and Abstract Interpretation

This page was built for publication: Dependently typed array programs don't go wrong