The Type Theory of PL/CV3

DOI10.1145/357233.357238zbMath0522.68020OpenAlexW1986382835MaRDI QIDQ3673081

Daniel R. Zlatin, Robert L. 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

specificationlambda calculustype theoryconstructive logiccombinatorsprogram verificationdata typesemantics of programming languagesautomated logic

Mathematics Subject Classification ID

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

Related Items

Innovations in computational type theory using Nuprl, On Church's formal theory of functions and functionals. The \(\lambda\)- calculus: Connections to higher type recursion theory, proof theory, category theory, Generalization from partial parametrization in higher-order type theory, Expressing computational complexity in constructive type theory, Type checking with universes, Static semantics, types, and binding time analysis, Unnamed Item