Extended Curry-Howard terms for second-order logic

DOI10.1002/MALQ.201100102MaRDI QIDQ2856633zbMATH OpenOpenAlexFDO

Authors Pimpen Vejjajiva

Publication date 30 October 2013

Published in Mathematical Logic Quarterly (MLQ) (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1002/malq.201100102

zbMATH Keywords

Curry-Howard termsextracting programs from proofssecond-order logic

Mathematics Subject Classification ID

Logic in computer science (03B70) Proof theory in general (including proof-theoretic semantics) (03F03) Cut-elimination and normal-form theorems (03F05) Other constructive mathematics (03F65)

Recommendations

• A direct proof of strong normalization for full constructive second-order logic
• scientific article; zbMATH DE number 749923
• Curry-Howard terms for linear logic
• Abbreviation templates
• New Curry-Howard terms for full linear logic

Cites work

• A direct proof of strong normalization for full constructive second-order logic
• Hauptsatz for higher order logic
• scientific article; zbMATH DE number 42059 (Why is no real title available?)
• scientific article; zbMATH DE number 749923 (Why is no real title available?)

Cited in

(5)

• New Curry-Howard terms for full linear logic
• Second-Order Equational Logic (Extended Abstract)
• scientific article; zbMATH DE number 1231518 (Why is no real title available?)
• Mendler-style iso-(co)inductive predicates: a strongly normalizing approach
• Abbreviation templates

This page was built for publication: Extended Curry-Howard terms for second-order logic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2856633)