Do-it-yourself type theory

DOI10.1007/BF01887198zbMath0697.68020OpenAlexW1997029640MaRDI QIDQ911744

Paul Chisholm, Erik Saaman, Grant Malcolm, 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

data structuresconstructive type theoryintuitionistic logicprogram development and correctnesspropositions-as-types

Mathematics Subject Classification ID

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

Related Items (12)

Inductive families ⋮ Program specification and data refinement in type theory ⋮ Semantics of under-determined expressions ⋮ Intuitionistic completeness of first-order logic ⋮ An intuitionistic theory of types with assumptions of high-arity variables ⋮ Tychonoff's theorem in the framework of formal topologies ⋮ Paramorphisms ⋮ Formalizing Type Operations Using the “Image” Type Constructor ⋮ ETA-RULES IN MARTIN-LÖF TYPE THEORY ⋮ MARTIN-LÖF'S TYPE THEORY AS AN OPEN-ENDED FRAMEWORK ⋮ A cartesian closed category in Martin-Löf's intuitionistic type theory ⋮ Normalising the associative law: An experiment with Martin-Löf's type theory

Uses Software

• Nuprl
• Automath

Cites Work

• Combinatory logic. With two sections by William Craig.
• Constructing recursion operators in intuitionistic type theory
• Derivation of a parsing algorithm in Martin-Löf's theory of types
• Terminating general recursion
• Type theory and concurrency
• Finding repeated elements
• A theory of type polymorphism in programming
• Representing inductively defined sets by wellorderings in Martin-Löf's type theory
• Writing programs that construct proofs
• Basic concepts for a theory of evaluation: Hierarchical aggregation via autodistributive connectives in fuzzy set theory
• Proof of correctness of data representations
• Constructive mathematics and computer programming
• A natural extension of natural deduction
• Predicative programming Part I
• A framework for defining logics
• Fast Pattern Matching in Strings
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

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