Comparing integrated and external logics of functional programs

DOI10.1016/0167-6423(90)90058-LzbMath0699.68025OpenAlexW2001176545MaRDI QIDQ913479

Peter Dybjer

Publication date: 1990

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

Full work available at URL: https://doi.org/10.1016/0167-6423(90)90058-l

zbMATH Keywords

Martin-Löf type theoryprogramming logicsAczel's logical theory of constructions

Mathematics Subject Classification ID

Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items (5)

Inductive families ⋮ A functional programming approach to the specification and verification of concurrent systems ⋮ Formal neighbourhoods, combinatory Böhm trees, and untyped normalization by evaluation ⋮ Normalising the associative law: An experiment with Martin-Löf's type theory ⋮ Synthesis of ML programs in the system Coq

This page was built for publication: Comparing integrated and external logics of functional programs