Dependently Typed Functional Programs and their Proofs Export

@misc{citeulike:5982826, abstract = {Research in dependent type theories [M-L71a] has, in the past, concentrated on its use in the presentation of theorems and theorem-proving. This thesis is concerned mainly with the exploitation of the computational aspects of type theory for programming, in a context where the properties of programs may readily be specified and established. In particular, it develops technology for programming with dependent inductive families of datatypes and proving those programs correct. It demonstrates the considerable advantage to be gained by indexing data structures with pertinent characteristic information whose soundness is ensured by typechecking, rather than human effort. Type theory traditionally presents safe and terminating computation on inductive datatypes by means of elimination rules which serve as induction principles and, via their associated reduction behaviour, recursion operators [Dyb91]. In the programming language arena, these appear somewhat cumbersome and give rise to unappe...}, author = {Mcbride, Conor}, citeulike-article-id = {5982826}, citeulike-linkout-0 = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.35.794}, keywords = {dependent-types, language-oleg, project-phd-thesis}, posted-at = {2009-10-21 20:26:22}, priority = {2}, title = {Dependently Typed Functional Programs and their Proofs}, url = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.35.794}, year = {1999} }

TY - ELEC ID - citeulike:5982826 L3 - citeulike-article-id:5982826 N2 - Research in dependent type theories [M-L71a] has, in the past, concentrated on its use in the presentation of theorems and theorem-proving. This thesis is concerned mainly with the exploitation of the computational aspects of type theory for programming, in a context where the properties of programs may readily be specified and established. In particular, it develops technology for programming with dependent inductive families of datatypes and proving those programs correct. It demonstrates the considerable advantage to be gained by indexing data structures with pertinent characteristic information whose soundness is ensured by typechecking, rather than human effort. Type theory traditionally presents safe and terminating computation on inductive datatypes by means of elimination rules which serve as induction principles and, via their associated reduction behaviour, recursion operators [Dyb91]. In the programming language arena, these appear somewhat cumbersome and give rise to unappe... TI - Dependently Typed Functional Programs and their Proofs KW - dependent-types KW - language-oleg KW - project-phd-thesis AU - Mcbride, Conor PY - 1999/// UR - http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.35.794 ER -