Thumbnail
Access Restriction
Open

Author Pfeifer, H. ♦ Rueß, H.
Source CiteSeerX
Content type Text
File Format PDF
Language English
Subject Domain (in DDC) Computer science, information & general works ♦ Data processing & computer science
Subject Keyword Polytypic Proof ♦ Mechanized Proof ♦ Polytypic Abstraction ♦ List Datatype ♦ Germany Fpfeifer ♦ Proof Editor ♦ Predefined Map Functional ♦ Type-theoretic Setting ♦ State Polytypic Theorem ♦ Fusion Theorem ♦ Large Class ♦ Main Advantage ♦ Target List ♦ Source List ♦ Polytypic Map Function ♦ Introduction Many Functional Programming Language ♦ Type Theory ♦ Polytypic Program ♦ Proof Construction ♦ Polytypic Formalization
Description ion in Type Theory H. Pfeifer and H. Rueß Universitat Ulm Fakultat fur Informatik D-89069 Ulm, Germany fpfeifer,ruessg@informatik.uni-ulm.de Abstract. This paper is concerned with formalizations and verifications in type theory that are abstracted with respect to a large class of datatypes; i.e polytypic formalizations. The main advantage of these developments are that they can not only be used to polytypically define functions but also to formally state polytypic theorems and to interactively develop polytypic proofs using existing proof editors. Polytypic program and proof construction in a type-theoretic setting is exemplified by the definition of a polytypic map function and by mechanized proofs of corresponding properties such as preservation of composition and fusion theorems. 1 Introduction Many functional programming languages provide a predefined map functional on the list datatype. Applying this functional to a function f and a source list l yields a target list obtained b...
Educational Role Student ♦ Teacher
Age Range above 22 year
Educational Use Research
Education Level UG and PG ♦ Career/Technical Study
Learning Resource Type Article
Publisher Date 1998-01-01
Publisher Institution Informal Proceedings of Workshop on Generic Programming (WGP98). Marstrand