Derivation of a parsing algorithm in Martin-Löf's theory of types

DOI10.1016/0167-6423(87)90002-5MaRDI QIDQ1097045zbMATH OpenOpenAlexFDO

Authors Paul Chisholm

Publication date 1987

Published in Science of Computer Programming (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/0167-6423(87)90002-5

zbMATH Keywords

correctness proof of specificationparsersimple expression languagetype theory

Mathematics Subject Classification ID

Second- and higher-order arithmetic and fragments (03F35) Theory of compilers and interpreters (68N20) Specification and verification (program logics, model checking, etc.) (68Q60) Abstract data types; algebraic specification (68Q65)

Review text

Type theory is a mathematical language with computation rules developed by Per Martin-Löf. Type theory was initially developed as a formalization of constructive mathematics but Martin-Löf has pointed out that it can also be viewed as a formal system for the development of provably correct programs. Here, a parser for a simple expression language is specified and a program derived from the proof of correctness of its specification using the formalism of type theory. The proof is compared with a proof of the same problem formalized in the Edinburgh LCF system.

Recommendations

• Program derivation in type theory: A partitioning problem
• scientific article; zbMATH DE number 559219
• scientific article; zbMATH DE number 140008
• On the syntax of Martin-Löf's type theories
• Do-it-yourself type theory

Cited in

(10)

• A simple type-theoretic language: Mini-TT
• Towards a theory of document structure
• Per Martin-Löf's type theory for automated program writing
• Program derivation in type theory: A partitioning problem
• scientific article; zbMATH DE number 140008 (Why is no real title available?)
• scientific article; zbMATH DE number 1156048 (Why is no real title available?)
• The epistemology of computer-mediated proofs
• A set constructor for inductive sets in Martin-Löf's type theory
• Normalising the associative law: An experiment with Martin-Löf's type theory
• Do-it-yourself type theory

Describes a project that uses

Uses Software

• LCF

This page was built for publication: Derivation of a parsing algorithm in Martin-Löf's theory of types

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