Types for Proofs and Programs

DOI10.1007/B98246zbMath1100.03516OpenAlexW4298423642MaRDI QIDQ5712312

Alwen Tiu, Alberto Momigliano

Publication date: 23 December 2005

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/b98246

Mathematics Subject Classification ID

Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Cut-elimination and normal-form theorems (03F05)

Related Items (14)

A two-level logic approach to reasoning about computations ⋮ Nominal abstraction ⋮ Unnamed Item ⋮ Cut elimination for a logic with induction and co-induction ⋮ Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax ⋮ Unnamed Item ⋮ Focused Inductive Theorem Proving ⋮ Least and Greatest Fixed Points in Linear Logic ⋮ Non-well-founded deduction for induction and coinduction ⋮ Dual Calculus with Inductive and Coinductive Types ⋮ Lexicographic Path Induction ⋮ A case study in programming coinductive proofs: Howe’s method ⋮ Unnamed Item ⋮ A Proof Theoretic Approach to Operational Semantics

Uses Software

• Isabelle/HOL

This page was built for publication: Types for Proofs and Programs