• Mathemagix

• Referenced in 42 articles [sw00553]
• symbolic and certified numeric algorithms. This language can be compiled and interpreted, and it features ... will illustrate possibilities offered for certified numeric computations with balls and intervals...

• GCminor

• Referenced in 4 articles [sw22622]
• certified framework for compiling and executing garbage-collected languages. We describe the design, implementation ... machine-certified framework for correct compilation and execution of programs in garbage-collected languages ... framework extends Leroy’s Coq-certified Compcert compiler and Cminor intermediate language...

• Template-Coq

• Referenced in 4 articles [sw27569]
• used in the CertiCoq certified compiler project [4], as its front-end language, to derive...

• CiaoPP

• Referenced in 45 articles [sw12089]
• assertions which cannot be checked completely at compile-time, etc. The abstract model ... analyzers is used in the system to certify that an untrusted mobile code is safe...

• WebAssembly

• Referenced in 1 article [sw40303]
• self-certifying compilation framework for WebAssembly. A self-certifying compiler is designed to generate ... design and implementation of a self-certifying compilation framework for WebAssembly, a new intermediate language...

• Fiat

• Referenced in 14 articles [sw21357]
• Fiat produces a formal proof trail certifying that the synthesized program meets the original specification ... equivalent OCaml program that can be compiled and run as normal...

• Jakarta

• Referenced in 18 articles [sw01269]
• refinement; the JaKarTa Prover Interface (JPI), a compiler that translates JSL specifications into proof assistants ... Goal of the work is to derive certified Byte Code Verifiers by abstraction from...

• MetaCoq

• Referenced in 1 article [sw40004]
• manipulating Coq terms and developing certified plugins (i.e. translations, compilers or tactics...

• IML - Integer Matrix Library

• Referenced in 16 articles [sw00440]
• integers. IML is designed to be compiled with a CBLAS library (e.g., ATLAS/BLAS ... right nullspace of an integer matrix. Certified linear system solving: compute a minimal denominator solution...

• FoCaLiZe

• Referenced in 10 articles [sw12384]
• providing a programming environment to develop certified programs. The environment is based on a functional ... FoCaLiZe source code development, the focalizec compiler produces three source files: a source file...

• Bedrock

• Referenced in 4 articles [sw28530]
• core combining characteristics of assembly languages and compiler intermediate languages. From this foundation, we take ... language”: we introduce an expressive notion of certified low-level macros, sufficient to build ... level of these macros only imposes a compile-time cost, via the execution of functional...

• Slicing

• Referenced in 1 article [sw29542]
• Towards Certified Slicing. Slicing is a widely-used technique with applications in e.g. compiler technology...

• MMTTeX

• Referenced in 2 articles [sw31595]
• communicating mathematical knowledge and the latter at certifying its correctness. MMTTeX aims at combining ... content during Open image in new window compilation and substitutes it with Open image...

• ACL2

• Referenced in 283 articles [sw00060]
• ACL2 is both a programming language in which...

• Coq

• Referenced in 1890 articles [sw00161]
• Coq is a formal proof management system. It...

• Dafny

• Referenced in 73 articles [sw00183]
• Dafny is an imperative object-based language with...

• Isabelle

• Referenced in 713 articles [sw00454]
• Isabelle is a generic proof assistant. It allows...

• Maple

• Referenced in 5373 articles [sw00545]
• The result of over 30 years of cutting...

• Mathematica

• Referenced in 6355 articles [sw00554]
• Almost any workflow involves computing results, and that...

• MiniSat

• Referenced in 566 articles [sw00577]
• An extensible SAT-solver. MiniSat is a minimalistic...