Do-it-yourself type theory

DOI10.1007/BF01887198MaRDI QIDQ911744zbMATH OpenOpenAlexFDO

Authors Paul Chisholm, Grant Malcolm, Erik Saaman, Roland C. Backhouse

Publication date 1989

Published in Formal Aspects of Computing (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/bf01887198

zbMATH Keywords

constructive type theorydata structuresintuitionistic logicprogram development and correctnesspropositions-as-types

Mathematics Subject Classification ID

Second- and higher-order arithmetic and fragments (03F35) Data structures (68P05) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• scientific article; zbMATH DE number 4096759
• scientific article; zbMATH DE number 559219
• scientific article; zbMATH DE number 4096760
• Propositions and specifications of programs in Martin-Löf's type theory
• scientific article; zbMATH DE number 2077110

Cites work

• A framework for defining logics
• A natural extension of natural deduction
• A theory of type polymorphism in programming
• Basic concepts for a theory of evaluation: Hierarchical aggregation via autodistributive connectives in fuzzy set theory
• Combinatory logic. With two sections by William Craig.
• Constructing recursion operators in intuitionistic type theory
• Constructive mathematics and computer programming
• Derivation of a parsing algorithm in Martin-Löf's theory of types
• Fast Pattern Matching in Strings
• Finding repeated elements
• scientific article; zbMATH DE number 4143955 (Why is no real title available?)
• scientific article; zbMATH DE number 3910392 (Why is no real title available?)
• scientific article; zbMATH DE number 3928338 (Why is no real title available?)
• scientific article; zbMATH DE number 3928956 (Why is no real title available?)
• scientific article; zbMATH DE number 3938546 (Why is no real title available?)
• scientific article; zbMATH DE number 3959364 (Why is no real title available?)
• scientific article; zbMATH DE number 3982493 (Why is no real title available?)
• scientific article; zbMATH DE number 3702108 (Why is no real title available?)
• scientific article; zbMATH DE number 3740740 (Why is no real title available?)
• scientific article; zbMATH DE number 3748394 (Why is no real title available?)
• scientific article; zbMATH DE number 50149 (Why is no real title available?)
• scientific article; zbMATH DE number 3574936 (Why is no real title available?)
• scientific article; zbMATH DE number 3630747 (Why is no real title available?)
• scientific article; zbMATH DE number 3894466 (Why is no real title available?)
• scientific article; zbMATH DE number 3073037 (Why is no real title available?)
• Predicative programming Part I
• Proof of correctness of data representations
• Representing inductively defined sets by wellorderings in Martin-Löf's type theory
• Terminating general recursion
• Type theory and concurrency
• Writing programs that construct proofs

Cited in

(38)

• A selected bibliography on constructive mathematics, intuitionistic type theory and higher order deduction
• Constructing recursion operators in intuitionistic type theory
• Derivation of a parsing algorithm in Martin-Löf's theory of types
• An intuitionistic theory of types with assumptions of high-arity variables
• Constructing type systems over an operational semantics
• Paramorphisms
• Constructing a theory of a data structure as an aid to program development
• Inductive families
• A cartesian closed category in Martin-Löf's intuitionistic type theory
• Semantics of under-determined expressions
• A type-theoretic approach to program development
• scientific article; zbMATH DE number 1678369 (Why is no real title available?)
• Type theory should eat itself
• Proof theory and computer programming
• scientific article; zbMATH DE number 3881865 (Why is no real title available?)
• scientific article; zbMATH DE number 3854400 (Why is no real title available?)
• scientific article; zbMATH DE number 3866573 (Why is no real title available?)
• Abstract Data Types and Type Theory: Theories as Types
• In the Search of a Naive Type Theory
• Per Martin-Löf's type theory for automated program writing
• A While-rule in Martin-Lof's Theory of Types
• scientific article; zbMATH DE number 4096759 (Why is no real title available?)
• scientific article; zbMATH DE number 4096760 (Why is no real title available?)
• Intuitionistic completeness of first-order logic
• Introducing data types in intuitionistic type theory
• scientific article; zbMATH DE number 1215502 (Why is no real title available?)
• scientific article; zbMATH DE number 1292292 (Why is no real title available?)
• Program specification and data refinement in type theory
• scientific article; zbMATH DE number 559219 (Why is no real title available?)
• Tychonoff's theorem in the framework of formal topologies
• Formalizing type operations using the ``image type constructor
• Applications of type theory
• Type theory as a foundation for computer science
• Eta-rules in Martin-Löf type theory
• Martin-Löf's type theory as an open-ended framework
• Native type theory
• Propositions and specifications of programs in Martin-Löf's type theory
• Normalising the associative law: An experiment with Martin-Löf's type theory

Describes a project that uses

Uses Software

• Automath
• Nuprl

This page was built for publication: Do-it-yourself type theory

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q911744)