Programming and Proving with Classical Types

DOI10.1007/978-3-319-71237-6_11zbMath1503.68046OpenAlexW2768246961MaRDI QIDQ5055999

Dominic P. Mulligan, Cristina Matache, Victor B. F. Gomes

Publication date: 9 December 2022

Published in: Programming Languages and Systems (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-319-71237-6_11

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Combinatory logic and lambda calculus (03B40) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Uses Software

• Matita
• Menhir
• Archive Formal Proofs
• OpenTheory

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Deriving a Floyd-Hoare logic for non-local jumps from a formulæ-as-types notion of control
• A syntactic theory of sequential control
• A strong normalization result for classical logic
• The \(\lambda \mu^{\mathbf{T}}\)-calculus
• Standalone Tactics Using OpenTheory
• ÜBER EINE BISHER NOCH NICHT BENÜTZTE ERWEITERUNG DES FINITEN STANDPUNKTES
• An environment machine for the λμ-calculus
• Proofs of strong normalisation for second order classical natural deduction
• A type-theoretic foundation of continuations and prompts
• The Matita Interactive Theorem Prover
• Bar recursion in classical realisability : dependent choice and continuum hypothesis
• The challenge of computer mathematics
• 30 years of research and development around Coq

This page was built for publication: Programming and Proving with Classical Types