Pages that link to "Item:Q3194730"

The following pages link to Interacting with Modal Logics in the Coq Proof Assistant (Q3194730):

Displaying 24 items.

• N. G. de Bruijn's contribution to the formalization of mathematics (Q740481) (← links)
• Resource operators for \(\lambda\)-calculus (Q876041) (← links)
• Certifying Findel derivatives for blockchain (Q2043802) (← links)
• Formally computing with the non-computable (Q2117773) (← links)
• Variants of Gödel's ontological proof in a natural deduction calculus (Q2363503) (← links)
• Exercising Nuprl’s Open-Endedness (Q2819194) (← links)
• Partiality, State and Dependent Types (Q3007667) (← links)
• Correct Code Containing Containers (Q3012966) (← links)
• Sawja: Static Analysis Workshop for Java (Q3067538) (← links)
• Certified Security Proofs of Cryptographic Protocols in the Computational Model: An Application to Intrusion Resilience (Q3100218) (← links)
• Proof Documents for Automated Origami Theorem Proving (Q3102737) (← links)
• Para-Disagreement Logics and Their Implementation Through Embedding in Coq and SMT (Q3305339) (← links)
• Invited Talk: On a (Quite) Universal Theorem Proving Approach and Its Application in Metaphysics (Q3455772) (← links)
• Arctic Termination ...Below Zero (Q3522019) (← links)
• An extensible equality checking algorithm for dependent type theories (Q5028472) (← links)
• Computer-supported Analysis of Positive Properties, Ultrafilters and Modal Collapse in Variants of Gödel's Ontological Argument (Q5126209) (← links)
• Injective types in univalent mathematics (Q5156770) (← links)
• Certified Reasoning with Infinity (Q5206958) (← links)
• Rigorous Estimation of Floating-Point Round-off Errors with Symbolic Taylor Expansions (Q5206960) (← links)
• Axiomatic and dual systems for constructive necessity, a formally verified equivalence (Q5231279) (← links)
• A general proof certification framework for modal logic (Q5236558) (← links)
• Algebraic Investigation of Connected Components (Q5283206) (← links)
• Reasoning About Cardinalities of Relations with Applications Supported by Proof Assistants (Q5283218) (← links)
• Certification of Proving Termination of Term Rewriting by Matrix Interpretations (Q5448658) (← links)