Simple Saturated Sets for Disjunction and Second-Order Existential Quantification

DOI10.1007/978-3-540-73228-0_26MaRDI QIDQ3612644zbMATH OpenOpenAlexFDO

Authors Makoto Tatsuta

Publication date 10 March 2009

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

Full work available at URL https://doi.org/10.1007/978-3-540-73228-0_26

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05)

Recommendations

• A simple proof of second-order strong normalization with permutative conversions
• scientific article; zbMATH DE number 1263308
• Strong normalization for non-structural subtyping via saturated sets
• Saturated formulas in full linear logic
• Non-strictly positive fixed points for classical natural deduction

Cited in

(8)

• Undecidability of Type-Checking in Domain-Free Typed Lambda-Calculi with Existence
• Type-Based Termination with Sized Products
• On the Values of Reducibility Candidates
• Polymorphic higher-order termination
• The existential fragment of second-order propositional intuitionistic logic is undecidable
• Strong normalization results by translation
• Inhabitation of polymorphic and existential types
• Disjoint essential sets of implicates of a CQ Horn function

This page was built for publication: Simple Saturated Sets for Disjunction and Second-Order Existential Quantification

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