Nonfree Datatypes in Isabelle/HOL - Animating a Many-Sorted Metatheory
Abstract elided by the publisher.
354 papers · page 16 of 18
Certified Kruskal's Tree Theorem
Abstract elided by the publisher.
Computational Verification of Network Programs in Coq
Abstract elided by the publisher.
A Formal Model and Correctness Proof for an Access Control Policy Framework
Abstract elided by the publisher.
Proof Pearl: Abella Formalization of λ-Calculus Cube Property
Abstract elided by the publisher.
Rating Disambiguation Errors
Abstract elided by the publisher.
Automation in Computer-Aided Cryptography: Proofs, Attacks and Designs
Abstract elided by the publisher.
Improving Real Analysis in Coq: A User-Friendly Approach to Integrals and Derivatives
Abstract elided by the publisher.
The New Quickcheck for Isabelle - Random, Exhaustive and Symbolic Testing under One Roof
Abstract elided by the publisher.
An Executable Semantics for CompCert C
Abstract elided by the publisher.
A String of Pearls: Proofs of Fermat's Little Theorem
Abstract elided by the publisher.
Compact Proof Certificates for Linear Logic
Abstract elided by the publisher.
Coherent and Strongly Discrete Rings in Type Theory
Abstract elided by the publisher.
Constructive Completeness for Modal Logic with Transitive Closure
Abstract elided by the publisher.
Program Certification by Higher-Order Model Checking
Abstract elided by the publisher.
Mechanized Semantics for Compiler Verification
Abstract elided by the publisher.
Scalable Formal Machine Models
Abstract elided by the publisher.
On the Correctness of an Optimising Assembler for the Intel MCS-51 Microprocessor
Abstract elided by the publisher.
Noninterference for Operating System Kernels
Abstract elided by the publisher.
Shall We Juggle, Coinductively?
Abstract elided by the publisher.