The SCEAS System
Navigation Menu

Conferences in DBLP

(itp)
2010 (conf/itp/2010)


  1. A Formally Verified OS Kernel. Now What? [Citation Graph (, )][DBLP]


  2. Proof Assistants as Teaching Assistants: A View from the Trenches. [Citation Graph (, )][DBLP]


  3. A Certified Denotational Abstract Interpreter. [Citation Graph (, )][DBLP]


  4. Using a First Order Logic to Verify That Some Set of Reals Has No Lesbegue Measure. [Citation Graph (, )][DBLP]


  5. A New Foundation for Nominal Isabelle. [Citation Graph (, )][DBLP]


  6. (Nominal) Unification by Recursive Descent with Triangular Substitutions. [Citation Graph (, )][DBLP]


  7. A Formal Proof of a Necessary and Sufficient Condition for Deadlock-Free Adaptive Networks. [Citation Graph (, )][DBLP]


  8. Extending Coq with Imperative Features and Its Application to SAT Verification. [Citation Graph (, )][DBLP]


  9. A Tactic Language for Declarative Proofs. [Citation Graph (, )][DBLP]


  10. Programming Language Techniques for Cryptographic Proofs. [Citation Graph (, )][DBLP]


  11. Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder. [Citation Graph (, )][DBLP]


  12. Formal Proof of a Wave Equation Resolution Scheme: The Method Error. [Citation Graph (, )][DBLP]


  13. An Efficient Coq Tactic for Deciding Kleene Algebras. [Citation Graph (, )][DBLP]


  14. Fast LCF-Style Proof Reconstruction for Z3. [Citation Graph (, )][DBLP]


  15. The Optimal Fixed Point Combinator. [Citation Graph (, )][DBLP]


  16. Formal Study of Plane Delaunay Triangulation. [Citation Graph (, )][DBLP]


  17. Reasoning with Higher-Order Abstract Syntax and Contexts: A Comparison. [Citation Graph (, )][DBLP]


  18. A Trustworthy Monadic Formalization of the ARMv7 Instruction Set Architecture. [Citation Graph (, )][DBLP]


  19. Automated Machine-Checked Hybrid System Safety Proofs. [Citation Graph (, )][DBLP]


  20. Coverset Induction with Partiality and Subsorts: A Powerlist Case Study. [Citation Graph (, )][DBLP]


  21. Case-Analysis for Rippling and Inductive Proof. [Citation Graph (, )][DBLP]


  22. Importing HOL Light into Coq. [Citation Graph (, )][DBLP]


  23. A Mechanized Translation from Higher-Order Logic to Set Theory. [Citation Graph (, )][DBLP]


  24. The Isabelle Collections Framework. [Citation Graph (, )][DBLP]


  25. Interactive Termination Proofs Using Termination Cores. [Citation Graph (, )][DBLP]


  26. A Framework for Formal Verification of Compiler Optimizations. [Citation Graph (, )][DBLP]


  27. On the Formalization of the Lebesgue Integration Theory in HOL. [Citation Graph (, )][DBLP]


  28. From Total Store Order to Sequential Consistency: A Practical Reduction Theorem. [Citation Graph (, )][DBLP]


  29. Equations: A Dependent Pattern-Matching Compiler. [Citation Graph (, )][DBLP]


  30. A Mechanically Verified AIG-to-BDD Conversion Algorithm. [Citation Graph (, )][DBLP]


  31. Inductive Consequences in the Calculus of Constructions. [Citation Graph (, )][DBLP]


  32. Validating QBF Invalidity in HOL4. [Citation Graph (, )][DBLP]


  33. Higher-Order Abstract Syntax in Isabelle/HOL. [Citation Graph (, )][DBLP]


  34. Separation Logic Adapted for Proofs by Rewriting. [Citation Graph (, )][DBLP]


  35. Developing the Algebraic Hierarchy with Type Classes in Coq. [Citation Graph (, )][DBLP]

NOTICE1
System may not be available sometimes or not working properly, since it is still in development with continuous upgrades
NOTICE2
The rankings that are presented on this page should NOT be considered as formal since the citation info is incomplete in DBLP
 
System created by asidirop@csd.auth.gr [http://users.auth.gr/~asidirop/] © 2002
for Data Engineering Laboratory, Department of Informatics, Aristotle University © 2002