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

automated logiccombinatorsconstructive logicdata typelambda calculusprogram verificationsemantics of programming languagesspecificationtype theory

Mathematics Subject Classification ID

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

Cited in

(7)

• On Church's formal theory of functions and functionals. The - calculus: Connections to higher type recursion theory, proof theory, category theory
• Generalization from partial parametrization in higher-order type theory
• Type checking with universes
• Static semantics, types, and binding time analysis
• A cubical language for Bishop sets
• Expressing computational complexity in constructive type theory
• Innovations in computational type theory using Nuprl

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)