Intuitionistic Ancestral Logic as a Dependently Typed Abstract Programming Language

DOI10.1007/978-3-662-47709-0_2zbMath1465.68036OpenAlexW1479185436MaRDI QIDQ2947456

Liron Cohen, Robert L. Constable

Publication date: 24 September 2015

Published in: Logic, Language, Information, and Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-662-47709-0_2

Mathematics Subject Classification ID

Theory of programming languages (68N15) Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Subsystems of classical logic (including intuitionistic logic) (03B20)

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Intuitionistic completeness of first-order logic
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Innovations in computational type theory using Nuprl
• Lectures on the Curry-Howard isomorphism
• Constructivism in mathematics. An introduction. Volume II
• Edinburgh LCF. A mechanized logic of computation
• On the Unusual Effectiveness of Logic in Computer Science
• Ancestral Logic: A Proof Theoretical Study
• A Brief Overview of Agda – A Functional Language with Dependent Types
• Proofs as programs
• A framework for defining logics
• The consistency of classical set theory relative to a set theory with intu1tionistic logic
• Automated Deduction – CADE-20

This page was built for publication: Intuitionistic Ancestral Logic as a Dependently Typed Abstract Programming Language