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

DOI10.1016/0167-6423(87)90002-5zbMath0634.68083OpenAlexW2031355212MaRDI QIDQ1097045

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

parsertype theorycorrectness proof of specificationsimple expression language

Mathematics Subject Classification ID

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

Related Items (3)

A set constructor for inductive sets in Martin-Löf's type theory ⋮ Do-it-yourself type theory ⋮ The Epistemology of Computer-Mediated Proofs

Uses Software

• LCF

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