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

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