Constructive ultra-filter theorem

For more info about our services contact : help@bestpfe.com

Table of contents

Acknowledgements
Introduction
Chapter 1. Constructive completeness for Boolean models
1.1. Historical overview
1.2. Constructive ultra-filter theorem
1.3. Constructive Henkin-style proof
1.4. Computational content
1.5. Aspects of the Coq formalisation
1.6. Related and future work
Chapter 2. Kripke-stylemodels for classical logic
2.1. Normalisation-by-evaluation as completeness
2.2. Sequent calculus LKμ˜μ
2.3. Kripke-style models, call-by-name variant
2.4. Kripke-style models, call-by-value variant
2.5. Computational content
2.6. Aspects of the Coq formalisation
2.7. Related and future work
Chapter 3. Kripke-stylemodels for intuitionistic logic
3.1. Historical overview
3.2. Type-directed partial evaluation for ¸-calculus with sum
3.3. Completeness for Kripke-style models
3.4. Computational content
3.5. Aspects of the Coq formalisation
3.6. Related and future work
Chapter 4. Extension of intuitionistic logic with delimited control
4.1. The systemMQC+
4.2. Relationship to MQC and CQC
4.3. Subject reduction and progress
4.4. Normalisation, disjunction and existence properties
4.5. Applications, related and future work
Bibliography
Appendix A. Additional material for MQC+
A.1. Call-by-name translation forMQC+
A.2. Explicit version of the two-level CPS transform