Propositions and specifications of programs in Martin-Löf's type theory

DOI10.1007/BF02136027zbMath0551.68027OpenAlexW2057584253MaRDI QIDQ800719

Bengt Nordström, Jan Smith

Publication date: 1984

Published in: BIT (Search for Journal in Brave)

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

zbMATH Keywords

program specificationMartin-Löf's type theorycompiler

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Abstract data types; algebraic specification (68Q65)

Related Items (7)

A theory of requirements capture and its applications ⋮ Constructing recursion operators in intuitionistic type theory ⋮ Terminating general recursion ⋮ Between constructive mathematics and PROLOG ⋮ An intuitionistic theory of types with assumptions of high-arity variables ⋮ The foundation of a generic theorem prover ⋮ A selected bibliography on constructive mathematics, intuitionistic type theory and higher order deduction

Uses Software

• Automath

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Combinatory logic. With two sections by William Craig.
• Constructions, proofs and the meaning of logical constants
• ÜBER EINE BISHER NOCH NICHT BENÜTZTE ERWEITERUNG DES FINITEN STANDPUNKTES
• A critique of the foundations of Hoare style programming logics
• A Transformation System for Developing Recursive Programs
• Can programming be liberated from the von Neumann style?
• On the interpretation of intuitionistic number theory

This page was built for publication: Propositions and specifications of programs in Martin-Löf's type theory