The Type Theory of PL/CV3

DOI10.1145/357233.357238zbMATH Open0522.68020OpenAlexW1986382835MaRDI QIDQ3673081FDOQ3673081

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 \(\lambda\)- calculus: Connections to higher type recursion theory, proof theory, category theory
• Title not available (Why is that?)

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)