The Type Theory of PL/CV3
From MaRDI portal
Publication:3673081
DOI10.1145/357233.357238zbMath0522.68020MaRDI QIDQ3673081
Robert L. Constable, Daniel R. Zlatin
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
specification; lambda calculus; type theory; constructive logic; combinators; program verification; data type; semantics of programming languages; automated logic
68Q60: Specification and verification (program logics, model checking, etc.)
68Q65: Abstract data types; algebraic specification
68N01: General topics in the theory of software
03B40: Combinatory logic and lambda calculus
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, Type checking with universes, Static semantics, types, and binding time analysis