Recent searches
Search options
#HOL_Light
A review on mechanical proving and formalization of mathematical theorems. ~ Si Chen, Wensheng Yu, Guowei Dou, Qimeng Zhang. https://ieeexplore.ieee.org/stamp/stamp.jsp?arnumber=10930874 #ITP #Coq #IsabelleHOL #HOL_Light #Mizar #LeanProver #Math
Readings shared January 26, 2025. https://jaalonso.github.io/vestigium/posts/2025/01/26-readings_shared_01-26-25 #ITP #LeanProver #HOL_Light #Math
Formalization of partial differential equations using HOL theorem proving. ~ Elif Deniz. https://hvg.ece.concordia.ca/Publications/Thesis/Elif-PhD-Thesis.pdf #ITP #HOL_Light #Math
Readings shared January 4, 2025. https://jaalonso.github.io/vestigium/posts/2025/01/04-readings_shared_01-04-25 #ITP #IsabelleHOL #LeanProver #HOL_Light #Mizar #Math #Logic #Haskell #Python
Growing HOLMS, a HOL Light library for modal systems. ~ Antonella Bilotta, Marco Maggesi, Cosimo Perini Brogi, Leonardo Quartini. https://overlay.uniud.it/workshop/2024/papers/paper5.pdf #ITP #HOL_Light #Logic
Readings shared September 28, 2024. https://jaalonso.github.io/vestigium/posts/2024/09/28-readings_shared_09-28-24 #ITP #LeanProver #IsabelleHOL #Coq #HOL_Light #Logic #Math
Formal verification of coupled transmission lines using theorem proving. ~ Elif Deniz, Adnan Rashid & Sofiène Tahar. https://hvg.ece.concordia.ca/projects/fvps/pde/Formal_Verification_of_Coupled_Transmission_Lines.pdf #ITP #HOL_Light
Readings shared September 14, 2024. https://jaalonso.github.io/vestigium/posts/2024/09/14-readings_shared_09-14-24 #ITP #LeanProver #Lean4 #IsabelleHOL #Agda #HOL_Light #Math #Haskell #FunctionalProgramming #LambdaCalculus #LLMs
Better-performing “25519” elliptic-curve cryptography (Automated reasoning and optimizations specific to CPU microarchitectures improve both performance and assurance of correct implementation). ~ Torben Hansen, John Harrison. https://www.amazon.science/blog/better-performing-25519-elliptic-curve-cryptography #ITP #HOL_Light
Lecturas compartidas el 25 de junio de 2024. https://jaalonso.github.io/vestigium/posts/2024/06/26-lecturas_compartidas_el_25-jun-24 #ITP #Agda #Coq #HOL #HOL_Light #IsabelleHOL #Lean4 #Metamath #Math #Haskell #Python #Algorithms #AI #MachineLearning
Lecturas compartidas el 6 de junio de 2024. https://jaalonso.github.io/vestigium/posts/2024/06/07-lecturas_compartidas_el_06-jun-24 #ITP #Lean4 #IsabelleHOL #HOL_Light #Math
The HOL Light library of formalized mathematics. ~ Marco Maggesi. https://europroofnet.github.io/_pages/WG4/Sep22/maggesi.pdf #ITP #HOL_Light #Math
Lecturas compartidas el 30 de mayo de 2024. https://jaalonso.github.io/vestigium/posts/2024/05/31-lecturas_compartidas_el_30-may-24 #ITP #Lean4 #IsabelleHOL #Coq #Theorema #HOL_Light #Math #ATP #Prover9 #Vampire #TPTP #FunctionalProgramming #Haskell #LogicProgramming #Prolog #AI #LLMs
Translating HOL-Light proofs to Coq. ~ Frédéric Blanqui. https://easychair.org/publications/paper/mtFT #ITP #HOL_Light #Coq
Lecturas compartidas el 11 de mayo de 2024. https://jalonso.substack.com/lecturas-compartidas-el-11-de-mayo #ITP #Lean4 #IsabelleHOL #Agda #Coq #HOL_Light #Metamath #Mizar #Math #Programming #CommonLisp
Algorithm and abstraction in formal mathematics. ~ Heather Macbeth. https://arxiv.org/abs/2405.04699 #ITP #Agda #Coq #Lean4 #HOL_Light #IsabelleHOL #Metamath #Mizar #Math