Dualized Simple Type Theory

DOI10.2168/LMCS-12(3:2)2016zbMath1445.03013arXiv1605.01083MaRDI QIDQ2974773

Ryan McCleeary, Aaron Stump, Harley III Eades

Publication date: 11 April 2017

Published in: Logical Methods in Computer Science (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1605.01083

zbMATH Keywords

dualconsistencycompletenesssequent calculusKripke modelcoinductionsimple type theorybi-intuitionistic logicexclusionsubtraction

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Subsystems of classical logic (including intuitionistic logic) (03B20) Combinatory logic and lambda calculus (03B40) Type theory (03B38)

Uses Software

• Ott

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Proof analysis in modal logic
• Copatterns
• The duality of computation
• Pragmatic and dialogic interpretations of bi-intuitionism. Part I
• Dual Calculus with Inductive and Coinductive Types
• Proof Search and Counter-Model Construction for Bi-intuitionistic Propositional Logic with Labelled Sequents
• Some Syntactical Observations on Linear Logic
• Semi-Boolean algebras and their applications to intuitionistic logic with dual operations
• A logic stronger than intuitionism
• A Formulae-as-Types Interpretation of Subtractive Logic
• Process Types as a Descriptive Tool for Interaction
• Ott: Effective tool support for the working semanticist
• A Connection-Based Characterization of Bi-intuitionistic Validity
• Computer Science Logic
• Term Rewriting and Applications
• Typed Lambda Calculi and Applications
• Subtractive logic