Abstract is missing.
- Efficient and Verified Continuous Double AuctionsMohit Garg 0003, Suneel Sarswat. 1-13 [doi]
- On SMT Theory Design: The Case of SequencesHichem Rami Ait El Hara, François Bobot, Guillaume Bury. 14-29 [doi]
- Alternate Semantics of the Guarded ConditionalNachum Dershowitz. 30-52 [doi]
- Certification of Tail Recursive Bubble-Sort in Theorema and CoqIsabela Dramnesc, Tudor Jebelean, Sorin Stratulat. 53-68 [doi]
- Automated Reasoning with Tangles: towards Quantum Verification ApplicationsAndrew Fish, Alexei Lisitsa 0001. 69-80 [doi]
- A System for Evaluating the Admissibility of Rules for Intuitionistic Propositional LogicAlexander V. Gheorghiu. 81-91 [doi]
- Numeric Base Conversion with RewritingOlivier Hermant, Wojciech Loboda. 92-106 [doi]
- A Natural-style Prover in Theorema Using Sequent Calculus with Unit PropagationTudor Jebelean. 107-116 [doi]
- On Proof Schemata and Primitive Recursive ArithmeticAlexander Leitsch, Anela Lolic, Stella Mahler. 117-130 [doi]
- Towards computer-assisted proofs of parametric Andrews-Curtis simplifications, IIAlexei Lisitsa 0001. 131-136 [doi]
- Automated Theorem Proving for Prolog VerificationFred Mesnard, Thierry Marianne, Étienne Payet. 137-151 [doi]
- On Symbolic Derivatives and Transition RegexesMargus Veanes. 152-162 [doi]
- A Case for Extensional Non-Wellfounded MetamodelingJoseph Zalewski, Pascal Hitzler. 163-178 [doi]