The following pages link to Programming Languages and Systems (Q5308710):
Displaying 12 items.
- A case study in formalizing projective geometry in Coq: Desargues theorem (Q448975) (← links)
- Trace-based verification of imperative programs with I/O (Q617977) (← links)
- An assertional proof of red-black trees using Dafny (Q1984797) (← links)
- A Coq Library for Internal Verification of Running-Times (Q2798271) (← links)
- Automatic Functional Correctness Proofs for Functional Search Trees (Q2829265) (← links)
- Verified Efficient Enumeration of Plane Graphs Modulo Isomorphism (Q3088012) (← links)
- Extraction in Coq: An Overview (Q3507450) (← links)
- Ready,<tt>Set</tt>, Verify! Applying<tt>hs-to-coq</tt>to real-world Haskell code (Q5018778) (← links)
- Extracting functional programs from Coq, in Coq (Q5101927) (← links)
- Building Certified Static Analysers by Modular Construction of Well-founded Lattices (Q5415621) (← links)
- (Q5875410) (← links)
- Efficient extensional binary tries (Q6156636) (← links)
