Coq
From MaRDI portal
Cited in
(only showing first 100 items - show all)- HasCasl: integrated higher-order specification and program development
- Programming languages and systems. 18th European symposium on programming, ESOP 2009, held as part of the joint European conferences on theory and practice of software, ETAPS 2009, York, UK, March 22--29, 2009. Proceedings
- Coinductive big-step operational semantics
- Certifying properties of an efficient functional program for computing Gröbner bases
- The RISC ProofNavigator: a proving assistant for program verification in the classroom
- Types for proofs and programs. International conference, TYPES 2008, Torino, Italy, March 26--29, 2008. Revised selected papers
- Using computer algebra techniques for the specification, verification and synthesis of recursive programs
- Intelligent computer mathematics. 16th symposium, Calculemus 2009, 8th international conference, MKM 2009, held as part of CICM 2009, Grand Bend, Canada, July 6--12, 2009. Proceedings
- Adapting functional programs to higher order logic
- Proof assistants: history, ideas and future
- A compact kernel for the calculus of inductive constructions
- Formalizing Arrow's theorem
- Data compression for proof replay
- A constructive approach to sequential Nash equilibria
- Verifying programs in the calculus of inductive constructions
- Types for proofs and programs. International workshop TYPES '96, Aussois, France, December 15--19, 1996. Selected papers
- A note on complexity measures for inductive classes in constructive type theory
- Automated synthesis of recursive programs from a logical specification
- Apron
- ACL2
- AXIOM
- A compositional -calculus proof system for statecharts processes
- Dafny
- On -conversion in the -cube and the combination with abbreviations
- GCLC
- HasCasl
- HYBRID
- Set theory for verification. I: From foundations to functions
- ILTP
- Isabelle
- Singleton, union, and intersection types for program extraction
- Synthesis of ML programs in the system Coq
- KeY-C
- LEDA
- LEO-II
- MetiTarski
- mizar-items
- MMP/Geometer
- binstretch
- Roosterize
- PCM library
- finmap
- ChvatalIP
- ROSMonitoring
- Marathon 2
- Inductive families
- Nitpick
- Ott
- PAG
- Proviola
- Focus points and convergent process operators: A proof strategy for protocol verification
- SPLAY
- DataFlasks
- ElasTest
- Minha
- CatTheo
- Goeland
- metalib
- Cubical Agda
- Harpoon
- solc-verify
- Braga Method
- ARQMath
- Statebox
- CQL
- idris-ct
- RelView
- HolPy
- Q#
- Formalizing process algebraic verifications in the calculus of constructions
- Automated theorem proving by test set induction
- Sawja
- SUBSEXPL
- Theorema
- TkWinHOL
- TPS
- Xeukleides
- Indexed types
- APS-1
- A compared study of two correctness proofs for the standardized algorithm of ABR conformance
- ML
- ALDOR
- Software security -- theories and systems. Mext-NSF-JSPS international symposium, ISSS 2002, Tokyo, Japan, November 8--10, 2002. Revised papers
- Alloy
- Rapide
- Stratego
- DrScheme
- Jakarta
- A rewriting approach to satisfiability procedures.
- A constructive algebraic hierarchy in Coq.
- Beluga
- Types for proofs and programs. International workshop, TYPES 2002, Berg en Dal, The Netherlands, April 24--28, 2002. Selected papers
- CLEAN
- PiDuce
- Theorem proving in higher order logics. 16th international conference, TPHOLs 2003, Rome, Italy, September 8--12, 2003. Proceedings
- COMBINE
- Typed lambda calculi and applications. 6th international conference, TLCA 2003, Valencia, Spain, June 10--12, 2003. Proceedings
- mCRL2
- Isabelle/HOL
- NeXeme
This page was built for software: Coq
