Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

project: Floating point mechanization for arith #394

Open
bollu opened this issue Jun 8, 2024 · 0 comments
Open

project: Floating point mechanization for arith #394

bollu opened this issue Jun 8, 2024 · 0 comments
Labels
potential-projects Projects that are well-scoped, suitable for writing a single paper or thesis on.

Comments

@bollu
Copy link
Collaborator

bollu commented Jun 8, 2024

We continue work on https://github.com/opencompl/HOLFloat-Lean/blob/main/HOLFloat/Fixed.lean, thereby making it the "standard" IEEE floating point semantics, with support for bitblasting, and connecting directly to Lean's computable content of floats.
@bollu bollu added the potential-projects Projects that are well-scoped, suitable for writing a single paper or thesis on. label Jun 8, 2024
@bollu bollu changed the title Floating point mechanization for arith project: Floating point mechanization for arith Jun 8, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
potential-projects Projects that are well-scoped, suitable for writing a single paper or thesis on.
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
1 participant
@bollu