Teaching Experience: Logic and Formal Methods with Coq
Abstract elided by the publisher.
354 papers · page 18 of 18
Proof Pearl: The Marriage Theorem
Abstract elided by the publisher.
The Teaching Tool CalcCheck A Proof-Checker for Gries and Schneider's "Logical Approach to Discrete Math"
Abstract elided by the publisher.
Reasoning about Constants in Nominal Isabelle or How to Formalize the Second Fixed Point Theorem
Abstract elided by the publisher.
Coq Mechanization of Featherweight Fortress with Multiple Dispatch and Multiple Inheritance
Abstract elided by the publisher.
Verification of Scalable Synchronous Queue
Abstract elided by the publisher.
A Proposal for Broad Spectrum Proof Certificates
Abstract elided by the publisher.
Hardware-Dependent Proofs of Numerical Programs
Abstract elided by the publisher.
Algebra, Logic, Locality, Concurrency
Abstract elided by the publisher.
Proof-Carrying Code in a Session-Typed Process Calculus
Abstract elided by the publisher.
Simple, Functional, Sound and Complete Parsing for All Context-Free Grammars
Abstract elided by the publisher.
First Steps towards the Certification of an ARM Simulator Using Compcert
The simulation of Systems-on-Chip (SoC) is nowadays a hot topic because, beyond providing many debugging facilities, it allows the development of dedicated software before the hardware is available. Low-consumption CPUs such as ARM play a central role in SoC. However, the effecti…
Automated Certification of Implicit Induction Proofs
Abstract elided by the publisher.
Univalent Semantics of Constructive Type Theories
Abstract elided by the publisher.