NDLI: Flocq: A Unified Library for Proving Floating-Point Algorithms in Coq

Please wait, while we are loading the content...

2015 IEEE 22nd Symposium on Computer Arithmetic

2013 IEEE 21st Symposium on Computer Arithmetic

2011 IEEE 20th Symposium on Computer Arithmetic

Table of Contents

Steering Committee

Symposium Committee

Program Committee

Additional Reviewers

Corporate Sponsors

High Intelligence Computing: The New Era of High Performance Computing

Short Division of Long Integers

High Degree Toom'n'Half for Balanced and Unbalanced Multiplication

Augmented Precision Square Roots and 2-D Norms, and Discussion on Correctly Rounding sqrt(x^2+y^2)

Towards a Quaternion Complex Logarithmic Number System

Composite Iterative Algorithm and Architecture for q-th Root Calculation

On the Fixed-Point Accuracy Analysis and Optimization of FFT Units with CORDIC Multipliers

Self Checking in Current Floating-Point Units

How to Square Floats Accurately and Efficiently on the ST231 Integer Processor

A 1.5 Ghz VLIW DSP CPU with Integrated Floating Point and Fixed Point Instructions in 40 nm CMOS

The POWER7 Binary Floating-Point Unit

Accelerating Computations on FPGA Carry Chains by Operand Compaction

Fast Ripple-Carry Adders in Standard-Cell CMOS VLSI

A Family of High Radix Signed Digit Adders

Fused Multiply-Add Microarchitecture Comprising Separate Early-Normalizing Multiply and Add Pipelines

Latency Sensitive FMA Design

The IBM zEnterprise-196 Decimal Floating-Point Accelerator

Radix-8 Digit-by-Rounding: Achieving High-Performance Reciprocals, Square Roots, and Reciprocal Square Roots

Tight Certification Techniques for Digit-by-Rounding Algorithms with Application to a New 1/sqrt(x) Design

Radix-16 Combined Division and Square Root Unit

A Prescale-Lookup-Postscale Additive Procedure for Obtaining a Single Precision Ulp Accurate Reciprocal

Teraflop FPGA Design

The Arithmetic Operators You Will Never See in a Microprocessor

Accelerating Large-Scale HPC Applications Using FPGAs

A General Approach for Improving RNS Montgomery Exponentiation Using Pre-processing

Bit-Sliced Binary Normal Basis Multiplication

Efficient SIMD Arithmetic Modulo a Mersenne Number

Automatic Generation of Code for the Evaluation of Constant Expressions at Any Precision with a Guaranteed Error Bound

Automatic Generation of Fast and Certified Code for Polynomial Evaluation

Flocq: A Unified Library for Proving Floating-Point Algorithms in Coq

Publisher's Information

2009 19th IEEE Symposium on Computer Arithmetic

18th IEEE Symposium on Computer Arithmetic (ARITH '07)

17th IEEE Symposium on Computer Arithmetic (ARITH'05)

Proceedings 2003 16th IEEE Symposium on Computer Arithmetic

Proceedings 15th IEEE Symposium on Computer Arithmetic. ARITH-15 2001

Proceedings 14th IEEE Symposium on Computer Arithmetic (Cat. No.99CB36336)

Proceedings 13th IEEE Sympsoium on Computer Arithmetic

Proceedings of the 12th Symposium on Computer Arithmetic

Proceedings of IEEE 11th Symposium on Computer Arithmetic

[1991] Proceedings 10th IEEE Symposium on Computer Arithmetic

Proceedings of 9th Symposium on Computer Arithmetic

1987 IEEE 8th Symposium on Computer Arithmetic (ARITH)

1985 IEEE 7th Symposium on Computer Arithmetic (ARITH)

1983 IEEE 6th Symposium on Computer Arithmetic (ARITH)

1981 IEEE 5th Symposium on Computer Arithmetic (ARITH)

1978 IEEE 4th Symposium onomputer Arithmetic (ARITH)

1975 IEEE 3rd Symposium on Computer Arithmetic (ARITH)

1972 IEEE 2nd Symposium on Computer Arithmetic (ARITH)

Flocq: A Unified Library for Proving Floating-Point Algorithms in Coq

Content Provider	IEEE Xplore Digital Library
Author	Boldo, S. Melquiond, G.
Copyright Year	2011
Abstract	Several formalizations of floating-point arithmetic have been designed for the Coq system, a generic proof assistant. Their different purposes have favored some specific applications: program verification, high-level properties, automation. Based on our experience using and/or developing these libraries, we have built a new system that is meant to encompass the other ones in a unified framework. It offers a multi-radix and multi-precision formalization for various floating- and fixed-point formats. This fresh setting has been the occasion for reevaluating known properties and generalizing them. This paper presents design decisions and examples of theorems from the Flocq system: a library easy to use, suitable for automation yet high-level and generic.
Starting Page	243
Ending Page	252
File Size	413280
Page Count	10
File Format	PDF
ISBN	9781424494576
ISSN	10636889
DOI	10.1109/ARITH.2011.40
Language	English
Publisher	Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Publisher Date	2011-07-25
Publisher Place	Germany
Access Restriction	Subscribed
Rights Holder	Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Subject Keyword	Libraries Automation Testing Humans Electronic mail Safety Arrays program verification floating-point arithmetic formal proof system
Content Type	Text
Resource Type	Article

Central Library (ISO-9001:2015 Certified)
Indian Institute of Technology Kharagpur
Kharagpur, West Bengal, India | PIN - 721302

See location in the Map
03222 282435
Mail: support@ndl.gov.in

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Library of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in