yusuke1997/dblp-id-title huggingface dataset:
Defining and Preserving More C Behaviors: Verified Compilation Using a Concrete Memory Model
A Mechanised Proof of the Time Invariance Thesis for the Weak Call-By-Value λ-Calculus
14th International Conference on Interactive Theorem Proving, ITP 2023, Białystok, Poland, July 31 - August 4, 2023
Deeper Shallow Embeddings
Reasoning with Higher-Order Abstract Syntax and Contexts: A Comparison
A Formal Proof of the Minor-Exclusion Property for Treewidth-Two Graphs
A Sound and Complete Projection for Global Types
On the Formalization of Z-Transform in HOL
Digitalization of HR management in government agencies
Towards Provably Robust Watermarking
A Formalized General Theory of Syntax with Bindings
Graphical Rewriting for Diagrammatic Reasoning in Monoidal Categories in Lean4 (Short Paper)
Refinement to Certify Abstract Interpretations, Illustrated on Linearization for Polyhedra
LCF-Style Bit-Blasting in HOL4
No Unification Variable Left Behind: Fully Grounding Type Inference for the HDM System
Animating the Formalised Semantics of a Java-Like Language
Antifounded Coinduction in Type Theory
Formalizing Concentration Inequalities in Rocq: Infrastructure and Automation
Fast LCF-Style Proof Reconstruction for Z3
Formalization of a Polymorphic Subtyping Algorithm
A Linear First-Order Functional Intermediate Language for Verified Compilers
CoSMed: A Confidentiality-Verified Social Media Platform
Mechanical Verification of SAT Refutations with Extended Resolution
Program Extraction from Nested Definitions
A Mechanized Theory of Regular Trees in Dependent Type Theory
Verifying That a Compiler Preserves Concurrent Value-Dependent Information-Flow Security
Abella: A Tutorial
The Functor of Points Approach to Schemes in Cubical Agda
Accelerating Verified-Compiler Development with a Verified Rewriting Engine
MDP + TA = PTA: Probabilistic Timed Automata, Formalized (Short Paper)
A Formalization of Convex Polyhedra Based on the Simplex Method
Declarative Proof Translation (Short Paper)
Using a First Order Logic to Verify That Some Set of Reals Has No Lesbegue Measure
Efficient, Verified Checking of Propositional Proofs
Proof Certificates in PVS
On the Formalization of the Lebesgue Integration Theory in HOL
Validating QBF Invalidity in HOL4
Modelling and Verifying Properties of Biological Neural Networks (Invited Talk)
Formalizing Colimits in 𝒞at
Towards Formal Foundations for Game Theory
Deriving Proved Equality Tests in Coq-Elpi: Stronger Induction Principles for Containers in Coq
Verified Efficient Enumeration of Plane Graphs Modulo Isomorphism
Flexible Coinduction in Agda
A Mechanically Verified AIG-to-BDD Conversion Algorithm
A Differential Operator Approach to Equational Differential Invariants - (Invited Paper)
Formalising Fisher's Inequality: Formal Linear Algebraic Proof Techniques in Combinatorics
A Formal Proof of R(4, 5)=25
Point-Free, Set-Free Concrete Linear Algebra
Program Verification in the Presence of Cached Address Translation
Steps towards Verified Implementations of HOL Light
A Verified Decision Procedure for Univariate Real Arithmetic with the BKR Algorithm
Deriving Comparators and Show Functions in Isabelle/HOL
Dependently Sorted Theorem Proving for Mathematical Foundations
Verifying a Sequent Calculus Prover for First-Order Logic with Functions in Isabelle/HOL
Mechanical Certification of Loop Pipelining Transformations: A Preview
ROSCoq: Robots Powered by Constructive Reals
Universe Polymorphism in Coq
Canonical Structures for the Working Coq User
A Natural Formalization of the Mutilated Checkerboard Problem in Naproche
(Nominal) Unification by Recursive Descent with Triangular Substitutions
Cardinalities of Finite Relations in Coq
Square Root and Division Elimination in PVS
Algebra Is Half the Battle: Verifying Presentations of Graded Unipotent Chevalley Groups
ProofWatch: Watchlist Guidance for Large Theories in E
Formalized, Effective Domain Theory in Coq
Stop When You Are Almost-Full - Adventures in Constructive Termination
A Trustworthy Monadic Formalization of the ARMv7 Instruction Set Architecture
Formalising Yoneda Ext in Univalent Foundations
Proof Pearl : Playing with the Tower of Hanoi Formally
Seventeen Provers Under the Hammer
Communicating Formal Proofs: The Case of Flyspeck
An Operational Semantics in Isabelle/HOL-CSP
Animating MRBNFs: Truly Modular Binding-Aware Datatypes in Isabelle/HOL
Modular Verification of Intrusive List and Tree Data Structures in Separation Logic
Structural Analysis of Narratives with the Coq Proof Assistant
Taming an Authoritative Armv8 ISA Specification: L3 Validation and CakeML Compiler Verification
Value-Oriented Legal Argumentation in Isabelle/HOL
Formal Verification of Optical Quantum Flip Gate
A Coq Formalization of Finitely Presented Modules
Decision support system for initiating projects of medical and social development in regions
Lessons for Interactive Theorem Proving Researchers from a Survey of Coq Users
Content-based encoding of mathematical and code libraries
Proving Quantum Programs Correct
Proof Tactics for Assertions in Separation Logic
Typing Total Recursive Functions in Coq
Termination Casts: A Flexible Approach to Termination with General Recursion
Reaching for the Star: Tale of a Monad in Coq
Verified Synthesis of Knowledge-Based Programs in Finite Synchronous Environments
Sledgehammering Without ATPs (Short Paper)
Potential implications of artificial intelligence for project management information systems
Interactive Theorem Proving - 7th International Conference, ITP 2016, Nancy, France, August 22-25, 2016, Proceedings
The Web of Mathematical Models: A Schema-based, Wiki-like, Interactive Platform
A Formalization of Dedekind Domains and Class Groups of Global Fields
Visual Theorem Proving with the Incredible Proof Machine
Formalizing Size-Optimal Sorting Networks: Extracting a Certified Proof Checker
Effect Polymorphism in Higher-Order Logic (Proof Pearl)
Certifying Voting Protocols
Verified Decision Procedures for Modal Logics
Programming Language Techniques for Cryptographic Proofs
From Total Store Order to Sequential Consistency: A Practical Reduction Theorem
Higher-Order Abstract Syntax in Isabelle/HOL
Interactive Theorem Proving - 9th International Conference, ITP 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 9-12, 2018, Proceedings
An Isabelle/HOL Formalisation of Green's Theorem
Stateless Higher-Order Logic with Quantified Types
Abstract, Compositional Consistency: Isabelle/HOL Locales for Completeness à la Fitting
Formalizing Splitting in Isabelle/HOL
Collaborative Interactive Theorem Proving with Clide
Formalizing the Divergence Theorem and the Cauchy Integral Formula in Lean
A Formal Proof in Coq of LaSalle's Invariance Principle
Constructive Final Semantics of Finite Bags
Verified Timing Transformations in Synchronous Circuits with \lambda \pi -Ware
Metadata for a wiki of formalized mathematics
Formal Verification of a Floating-Point Expansion Renormalization Algorithm
Automatic Differentiation in ACL2
Synthesis of Safe Pointer-Manipulating Programs (Invited Talk)
Homotopy Type Theory in Lean
Nondeterministic Asynchronous Dataflow in Isabelle/HOL
Software Tool Support for Modular Reasoning in Modal Logics of Actions
Canonical for Automated Theorem Proving in Lean
Project of an information system for restaurant business management
A Mechanized Proof of the Max-Flow Min-Cut Theorem for Countable Networks
Bel-Games: A Formal Theory of Games of Incomplete Information Based on Belief Functions in the Coq Proof Assistant
Interactive Theorem Proving - Second International Conference, ITP 2011, Berg en Dal, The Netherlands, August 22-25, 2011. Proceedings
Proof Pearl: Proving a Simple Von Neumann Machine Turing Complete
A Variant of Wagner's Theorem Based on Combinatorial Hypermaps
A Verified Cost Model for Call-By-Push-Value
Formalized Haar Measure
Nine Chapters of Analytic Number Theory in Isabelle/HOL
Identification of priority objects for the implementation of projects to restore the transport infrastructure of settlements in the post-war period
Bounded-Deducibility Security (Invited Paper)
Mechanical Verification of a Constructive Proof for FLP
Now It Compiles! Certified Automatic Repair of Uncompilable Protocols
Compositional Verification of Interacting Systems Using Event Monads
seL4 Enforces Integrity
Proof Repair Infrastructure for Supervised Models: Building a Large Proof Repair Dataset
Distributed Parallel Build for the Isabelle Archive of Formal Proofs
Recursive Definitions of Monadic Functions
Formalization of Shannon's Theorems in SSReflect-Coq
Unified Decision Procedures for Regular Expression Equivalence
Priority Inheritance Protocol Proved Correct
Infeasible Paths Elimination by Symbolic Execution Techniques - Proof of Correctness and Preservation of Paths
Formal C Semantics: CompCert and the C Standard
Verified Abstract Interpretation Techniques for Disassembling Low-level Self-modifying Code
A Consistent Foundation for Isabelle/HOL
Asynchronous User Interaction and Tool Integration in Isabelle/PIDE
10th International Conference on Interactive Theorem Proving, ITP 2019, Portland, OR, USA, September 9-12, 2019
Developing the Algebraic Hierarchy with Type Classes in Coq
A Formal Equational Theory for Call-By-Push-Value
How to Simulate It in Isabelle: Towards Formal Proof for Secure Multi-Party Computation
Itauto: An Extensible Intuitionistic SAT Solver
Interactive Theorem Proving - 5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings
A Mechanized First-Order Theory of Algebraic Data Types with Pattern Matching
CompCertS: A Memory-Aware Verified C Compiler Using Pointer as Integer Semantics
Dynamic Proof Pages
Verifying Software Emulation of an Unsupported Hardware Instruction
What's in a Theorem Name?
Management of the IT project as a complex system
Homotopy Type Theory in Isabelle
An Isabelle/HOL Formalization of Narrowing and Multiset Narrowing for E-Unifiability, Reachability and Infeasibility
Proof-Producing Reflection for HOL - With an Application to Model Polymorphism
Case-Analysis for Rippling and Inductive Proof
Implementing More Explicit Definitional Expansions in Mizar (Short Paper)
Automating Theorem Proving with SMT
A Language of Patterns for Subterm Selection
Mechanized HOL Reasoning in Set Theory
ModuRes: A Coq Library for Modular Reasoning About Concurrent Higher-Order Imperative Programming Languages
Fast Machine Words in Isabelle/HOL
On Verifying Secret Control Flow Elimination
Formalisation of Additive Combinatorics in Isabelle/HOL (Invited Talk)
Towards Solid Abelian Groups: A Formal Proof of Nöbeling's Theorem
Formal Proofs of Tarjan's Strongly Connected Components Algorithm in Why3, Coq and Isabelle
Automatically Generated Infrastructure for De Bruijn Syntaxes
Verified Double Sided Auctions for Financial Markets
Robust Mean Estimation by All Means (Short Paper)
Specifying Message Formats with Contiguity Types
A Graphical User Interface Framework for Formal Verification
A Formal Analysis of Capacity Scaling Algorithms for Minimum Cost Flows
Type Classes and Filters for Mathematical Analysis in Isabelle/HOL
Program Analysis and Verification Based on Kleene Algebra in Isabelle/HOL
Mechanising Böhm Trees and λη-Completeness
Amortized Complexity Verified
Modular Dependent Induction in Coq, Mendler-Style
Correctly Compiling Proofs About Programs Without Proving Compilers Correct
Formalizing Basic Quaternionic Analysis
Conceptual model of the face recognition process based on the image of the face and iris of personnel of critical infrastructure facilities
A Formalisation of the Myhill-Nerode Theorem Based on Regular Expressions (Proof Pearl)
A Formal Proof of a Necessary and Sufficient Condition for Deadlock-Free Adaptive Networks
MaSh: Machine Learning for Sledgehammer
Primitive Floats in Coq
Group Cohomology in the Lean Community Library
Towards Verification of Product Lines
Standalone Tactics Using OpenTheory
Formalizing a Diophantine Representation of the Set of Prime Numbers
Verified Memoization and Dynamic Programming
Translating Libraries of Definitions and Theorems Between Proof Systems (Invited Talk)
A Formalization of the LLL Basis Reduction Algorithm
A Modular Formalization of Superposition in Isabelle/HOL
From Types to Sets by Local Type Definitions in Higher-Order Logic
Formally Verified Safe Vertical Maneuvers for Non-deterministic, Accelerating Aircraft Dynamics
Abstractions for Multi-Sorted Substitutions
A Parallelized Theorem Prover for a Logic with Parallel Execution
Completeness and Decidability Results for CTL in Coq
Two-Way Automata in Coq
Formalizing Norm Extensions and Applications to Number Theory
A Coq Formalisation of SQL's Execution Engines
A Formal Proof of Modal Completeness for Provability Logic
Formalization of Error-Correcting Codes: From Hamming to Modern Coding Theory
Inductive Predicates via Least Fixpoints in Higher-Order Separation Logic
Fast, Verified Computation for Candle
Verifying a Concurrent Garbage Collector Using a Rely-Guarantee Methodology
Use and Abuse of Instance Parameters in the Lean Mathematical Library
Supply chain management information system project with the use of digital twins
Compositional Computational Reflection
Alpha-Beta Pruning Verified (Invited Talk)
Certification of Nontermination Proofs
Formalizing the Algebraic Small Object Argument in UniMath
Formalizing the Solution to the Cap Set Problem
Microcode Verification - Another Piece of the Microprocessor Verification Puzzle
A Concrete Memory Model for CompCert
Certification of Classical Confluence Results for Left-Linear Term Rewrite Systems
Functional Programs: Conversions between Deep and Shallow Embeddings
HOL Constant Definition Done Right
A Formal Proof of the Expressiveness of Deep Learning
A Formally Verified Solver for Homogeneous Linear Diophantine Equations
Efficient Mendler-Style Lambda-Encodings in Cedille
End-To-End Formal Verification of a Fast and Accurate Floating-Point Approximation
Autosubst: Reasoning with de Bruijn Terms and Parallel Substitutions
Mechanised Separation Algebra
A Formal Proof of Complexity Bounds on Diophantine Equations
Recursive Functions on Lazy Lists via Domains and Topologies
Wiki Authoring and Semantics of Mathematical Document Structure
Challenges in Verifying Communication Fabrics
Certifying Higher-Order Polynomial Interpretations
Towards a Formally Verified Proof Assistant
Schulze Voting as Evidence Carrying Computation
Balancing Lists: A Proof Pearl
Proving Tree Algorithms for Succinct Data Structures
Bellerophon: Tactical Theorem Proving for Hybrid Systems
Verified Spilling and Translation Validation with Repair
Formal Proof of a Wave Equation Resolution Scheme: The Method Error
Pragmatic Quotient Types in Coq
Circular Coinduction in Coq Using Bisimulation-Up-To Techniques
The Coinductive Formulation of Common Knowledge
Handcrafted Inversions Made Operational on Operational Semantics
Verification of PCP-Related Computational Reductions in Coq
Refinement of Parallel Algorithms down to LLVM
MizAR 60 for Mizar 50
Mechanising Turing Machines and Computability Theory in Isabelle/HOL
An Efficient Coq Tactic for Deciding Kleene Algebras
Proof Pearl: A Probabilistic Proof for the Girth-Chromatic Number Theorem
Syntactic-Semantic Form of Mizar Articles
Generating Verified LLVM from Isabelle/HOL
The Rewster: Type Preserving Rewrite Rules for the Coq Proof Assistant
From Operational Models to Information Theory; Side Channels in pGCL with Isabelle
Formalizing Results on Directed Sets in Isabelle/HOL (Proof Pearl)
Interactive Termination Proofs Using Termination Cores
HOL Light QE
Verified Progress Tracking for Timely Dataflow
Affine Arithmetic and Applications to Real-Number Proving
Formalization of Randomized Approximation Algorithms for Frequency Moments
Interactive Theorem Proving - 8th International Conference, ITP 2017, Brasília, Brazil, September 26-29, 2017, Proceedings
A Tactic Language for Declarative Proofs
A Verified Compositional Algorithm for AI Planning
Improving the SMT Proof Reconstruction Pipeline in Isabelle/HOL
Formalising Knot Theory in Isabelle/HOL
General Recursion and Formal Topology
An Isabelle/HOL Formalization of Semi-Thue and Conditional Semi-Thue Systems
Ordinals in HOL: Transfinite Arithmetic up to (and Beyond) ω 1
MiniAgda: Integrating Sized and Dependent Types
A Certifying Extraction with Time Bounds from Coq to Call-By-Value Lambda Calculus
A Heuristic Prover for Real Inequalities
A Complete, Mechanically-Verified Proof of the Banach-Tarski Theorem in ACL2(R)
Hereditarily Finite Sets in Constructive Type Theory
Formalising the Proj Construction in Lean
Formalising Half of a Graduate Textbook on Number Theory (Short Paper)
User Interface Design in the HolPy Theorem Prover (Invited Talk)
Coverset Induction with Partiality and Subsorts: A Powerlist Case Study
The project formation of virtual graphic images in applications for distance education systems
Practical Probability: Applying pGCL to Lattice Scheduling
MetiTarski: Past and Future
Formalising Inductive and Coinductive Containers
Teaching Mathematics Using Lean and Controlled Natural Language
Formalising New Mathematics in Isabelle: Diagonal Ramsey
An Isabelle Proof Method Language
Weak Call-by-Value Lambda Calculus as a Model of Computation in Coq
Automated Theorem Proving for Metamath
A Formal Analysis of RANKING
Importing HOL Light into Coq
Formalising Subject Reduction and Progress for Multiparty Session Processes
Verifying Datalog Reasoning with Lean
Mechanising Complexity Theory: The Cook-Levin Theorem in Coq
Formalization of the Domination Chain with Weighted Parameters (Short Paper)
Towards Robustness Analysis Using PVS
A Refinement-Based Approach to Computational Algebra in Coq
The Directed Van Kampen Theorem in Lean
Verified Over-Approximation of the Diameter of Propositionally Factored Transition Systems
Application of a Genetic Approach to the Formation of Object Characteristics in Project Products
"Clip" thinking as the tool of Agile project management in an artificial intelligence environment
Separation Logic Adapted for Proofs by Rewriting
A Verified Generate-Test-Aggregate Coq Library for Parallel Programs Extraction
Formalization of Entropy Measures in HOL
Experience Implementing a Performant Category-Theory Library in Coq
Are We There Yet? 20 Years of Industrial Theorem Proving with SPARK
Semantic Foundations of Higher-Order Probabilistic Programs in Isabelle/HOL
Truly Modular (Co)datatypes for Isabelle/HOL
Termination Checking in the Presence of Nested Inductive and Coinductive Types
Applying Formal Methods in the Large
Formal Study of Plane Delaunay Triangulation
Interactive Theorem Proving - 6th International Conference, ITP 2015, Nanjing, China, August 24-27, 2015, Proceedings
Making PVS Accessible to Generic Services by Interpretation in a Universal Format
A Million Lines of Proof About a Moving Target (Invited Talk)
CoqPIE: An IDE Aimed at Improving Proof Development Productivity - (Rough Diamond)
Hammering Mizar by Learning Clause Guidance (Short Paper)
Numerical Analysis of Ordinary Differential Equations in Isabelle/HOL
Formal Program Optimization in Nuprl Using Computational Equivalence and Partial Types
Enhancing Urban Planning with LoRa and GANs: A Project Management Perspective
A Generalised Union of Rely-Guarantee and Separation Logic Using Permission Algebras
Barendregt's Theory of the λ-Calculus, Refreshed and Formalized
Verifying and Generating WP Transformers for Procedures on Complex Data
Cyclic Proofs and Coinductive Principles
Proof Pearl: Bounding Least Common Multiples with Triangles
The analysis of the optimum equilibrium to a game and theory model of hierarchic game under conditions of a mixed joint project management
Inductive Consequences in the Calculus of Constructions
Learning to Parse on Aligned Corpora (Rough Diamond)
Rewriting and Well-Definedness within a Proof System
Towards Certifying Network Calculus
On the Generation of Positivstellensatz Witnesses in Degenerate Cases
POSIX Lexing with Bitcoded Derivatives
Automatically Generalizing Proofs and Statements
Mostly Automated Formal Verification of Loop Dependencies with Applications to Distributed Stencil Algorithms
Boosting the Reuse of Formal Specifications
A Cantor Trio: Denumerability, the Reals, and the Real Algebraic Numbers
Backwards and Forwards with Separation Logic
Genetic Algorithm for Maritime Route Planning Projects with Improved Constraints
Proving Valid Quantified Boolean Formulas in HOL Light
HOCore in Coq
A Formalization of Polytime Functions
A Formalization of Forcing and the Unprovability of the Continuum Hypothesis
The Optimal Fixed Point Combinator
Formal Verification of Termination Criteria for First-Order Recursive Functions
Duper: A Proof-Producing Superposition Theorem Prover for Dependent Type Theory
A Formalization of Divided Powers in Lean
Mechanised Computability Theory
A Certified Proof Checker for Deep Neural Network Verification in Imandra
The Reflective Milawa Theorem Prover Is Sound - (Down to the Machine Code That Runs It)
A Formally Verified Checker for First-Order Proofs
Formalizing Computability Theory via Partial Recursive Functions
Algebraic Numbers in Isabelle/HOL
A Framework for the Automatic Formal Verification of Refinement from Cogent to C
Taming Differentiable Logics with Coq Formalisation
Stream Fusion for Isabelle's Code Generator - Rough Diamond
A Formally Verified OS Kernel. Now What?
Verified Efficient Implementation of Gabow's Strongly Connected Component Algorithm
Implicational Rewriting Tactics in HOL
A New Foundation for Nominal Isabelle
A Certificate-Based Approach to Formally Verified Approximations
LISA - A Modern Proof System
The Zoo of Lambda-Calculus Reduction Strategies, And Coq
A Natural Language Formalization of Perfectoid Rings in ℕaproche
Verification of the CVM Algorithm with a Functional Probabilistic Invariant
Unsolvability of the Quintic Formalized in Dependent Type Theory
Virtualization of HOL4 in Isabelle
Equational Reasoning with Applicative Functors
Ideas for a MathWiki Editor
Formalizing the Hidden Number Problem in Isabelle/HOL
Interactive Theorem Proving - Third International Conference, ITP 2012, Princeton, NJ, USA, August 13-15, 2012. Proceedings
GOL in GOL in HOL: Verified Circuits in Conway's Game of Life
Completeness of Asynchronous Session Tree Subtyping in Coq
Lightweight Proof by Reflection Using a Posteriori Simulation of Effectful Computation
An Extensible User Interface for Lean 4
Taming Floating-Point Rounding Errors with Proofs (Invited Talk)
A Verified LL(1) Parser Generator
Quantitative Continuity and Computable Analysis in Coq
Proceedings of the ITP 2011 Workshop on Mathematical Wikis, Nijmegen, The Netherlands, August 27th, 2011
Strategizing VR Integration in Business and Education: Extending the Technology Acceptance Model through Project Management Perspectives
Formally Verifying a Vertical Cell Decomposition Algorithm
Dandelion: Certified Approximations of Elementary Functions
Verified Analysis of Random Binary Tree Structures
HOL with Definitions: Semantics, Soundness, and a Verified Implementation
Closure Properties of General Grammars - Formally Verified
Undecidability of Dyadic First-Order Logic in Coq
Pattern Matches in HOL: - A New Representation and Improved Code Generation
Fermat's Last Theorem for Regular Primes (Short Paper)
Management of digitization of infrastructure projects and programs
LeanLTL: A Unifying Framework for Linear Temporal Logics in Lean (Short Paper)
Parameterized biorthogonal wavelet lifting for lightweight JPEG 2000 transparent encryption
Multimedia and Security Workshop, MM&Sec 2010, Roma, Italy, September 9-10, 2010
Steganalysis of GIM-based data hiding using kernel density estimation
On achievable security levels for lattice data hiding in the known message attack scenario
Reverse-engineer methods on a biometric hash algorithm for dynamic handwriting
Two key estimation techniques for the broken arrows watermarking scheme
Proceedings of the 6th workshop on Multimedia & Security, MM&Sec 2004, Magdeburg, Germany, September 20-21, 2004
Extraction in software watermarking
Distributed keyless security for correlated data with applications in visual sensor networks
Secure fingerprint-based authentication for Lotus Notes®