The Type Theory of PL/CV3

DOI10.1145/357233.357238MaRDI QIDQ3673081zbMATH OpenOpenAlexFDO

Authors Daniel R. Zlatin, Robert Constable

Publication date 1984

Published in ACM Transactions on Programming Languages and Systems (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/357233.357238

zbMATH Keywords

constructive logicspecificationtype theorylambda calculusprogram verificationcombinatorsdata typesemantics of programming languagesautomated logic

Mathematics Subject Classification ID

General topics in the theory of software (68N01) Specification and verification (program logics, model checking, etc.) (68Q60) Combinatory logic and lambda calculus (03B40) Abstract data types; algebraic specification (68Q65)

Cited in

(7)

• Expressing computational complexity in constructive type theory
• Generalization from partial parametrization in higher-order type theory
• Type checking with universes
• Static semantics, types, and binding time analysis
• Innovations in computational type theory using Nuprl
• On Church's formal theory of functions and functionals. The - calculus: Connections to higher type recursion theory, proof theory, category theory
• scientific article; zbMATH DE number 7566056 (Why is no real title available?)

This page was built for publication: The Type Theory of PL/CV3

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