Efficient Reasoning about Executable Specifications in Coq
- 25 July 2002
- book chapter
- Published by Springer Nature
Abstract
No abstract availableKeywords
This publication has 10 references indexed in Scilit:
- Inductive definitions in the system Coq rules and propertiesPublished by Springer Nature ,2005
- A Formal Correspondence between Offensive and Defensive JavaCard Virtual MachinesPublished by Springer Nature ,2002
- Executing Higher Order LogicPublished by Springer Nature ,2002
- Jakarta: A Toolset for Reasoning about JavaCardPublished by Springer Nature ,2001
- A Formal Executable Semantics of the JavaCard PlatformPublished by Springer Nature ,2001
- Automated Theorem Proving by Test Set InductionJournal of Symbolic Computation, 1997
- ELANElectronic Notes in Theoretical Computer Science, 1996
- Encoding natural semantics in CoqPublished by Springer Nature ,1995
- Elf: A meta-language for deductive systemsPublished by Springer Nature ,1994
- IsabellePublished by Springer Nature ,1994