yusuke1997/dblp-id-title huggingface dataset:
Perfect Number Theorem
Stellar Quorum Systems
Turán's Graph Theorem
A Dependent Security Type System for Concurrent Imperative Programs
The Laws of Large Numbers
The Boustrophedon Transform, the Entringer Numbers, and Related Sequences
Dynamic Architectures
Simultaneous diagonalization of pairwise commuting Hermitian matrices
A verified LLL algorithm
Linear Recurrences
Towards Certified Slicing
A formal model for the SPARCv8 ISA and a proof of non-interference for the LEON3 processor
Lp spaces
Power Sum Polynomials
The Floyd-Warshall Algorithm for Shortest Paths
VerifyThis 2019 - Polished Isabelle Solutions
Hood-Melville Queue
Stratified Datalog and Program Analysis
Knuth-Morris-Pratt String Search
The Imperative Refinement Framework
Formalization of Gyrovector Spaces as Models of Hyperbolic Geometry and Special Relativity
Dedekind Sums
Partial Semigroups and Convolution Algebras
Anselm's God in Isabelle/HOL
A Proof from THE BOOK: The Partial Fraction Expansion of the Cotangent
A Separation Logic Framework for Imperative HOL
Szemerédi's Regularity Lemma
Knowledge-based programs
Linear Resources and Process Compositions
Declarative Semantics for Functional Languages
Suppes' Theorem For Probability Logic
A Formal Proof of the Max-Flow Min-Cut Theorem for Countable Networks
Latin Square
Real Exponents as the Limits of Sequences of Rational Exponents
Executable Multivariate Polynomials
Gröbner Bases, Macaulay Matrices and Dubé's Degree Bounds
Semantics and Data Refinement of Invariant Based Programs
Rank-Nullity Theorem in Linear Algebra
Surprise Paradox
A Formal Model of IEEE Floating Point Arithmetic
A Mechanically Verified, Efficient, Sound and Complete Theorem Prover For First Order Logic
CryptHOL
Algorithms for Reduced Ordered Binary Decision Diagrams
Topological Groups
Authenticated Data Structures As Functors
A Modular Formalization of Superposition
Bondy's Theorem
Poincaré Disc Model
Information Flow Control via Dependency Tracking
A Verified Reduction Algorithm from MLSSmf to MLSS
The Elementary Theory of the Category of Sets
Formalizing a Seligman-Style Tableau System for Hybrid Logic
Verifying Imperative Programs using Auto2
Affine Arithmetic
Formalization of Nested Multisets, Hereditary Multisets, and Syntactic Ordinals
Formalization of a Framework for the Sound Automation of Magic Wands
A Modular Splitting Framework for Saturation Theorem Proving
Hybrid Multi-Lane Spatial Logic
Abstract Object Theory
Go Code Generation for Isabelle
Compositional Properties of Crypto-Based Components
Propositional Proof Systems
Mechanization of the Algebra for Wireless Networks (AWN)
Well-Quasi-Orders
First Order Clause
A formalized programming language with speculative execution
Epistemic Logic
Multi-Party Computation
Analysis of List Update Algorithms
AutoCorres2
Isabelle/Circus
Hilbert's Nullstellensatz
Elementary Facts About the Distribution of Primes
A Formal Model of the Safely Composable Document Object Model with Shadow Roots
An Isabelle/HOL formalisation of Green's Theorem
Formalizing Neural Networks
Formalization of an Optimized Monitoring Algorithm for Metric First-Order Dynamic Logic with Aggregations
Path Equivalence and Automation for Integration Contours
Relative Security
A verified factorization algorithm for integer polynomials with polynomial complexity
Faithful Logic Embeddings in HOL - Deep and Shallow (Isabelle/HOL dataset)
Wieferich-Kempner Theorem
Residuated Transition Systems
Dirichlet Series
Mini ML
Binomial Heaps and Skew Binomial Heaps
Gröbner Bases Theory
Babai's Nearest Plane Algorithm
Polygonal Number Theorem
The Inversions of a List
Kummer's congruence
Binary Heaps for IMP2
A Constructive Proof for FLP
Euler's Partition Theorem
Safe OCL
Executable Randomized Algorithms
Noninterference Security in Communicating Sequential Processes
The Inductive Unwinding Theorem for CSP Noninterference Security
Infeasible Paths Elimination by Symbolic Execution Techniques: Proof of Correctness and Preservation of Paths
Intersection of two monoids generated by two element codes
Formalizing Coppersmith's Method
Randomised Binary Search Trees
Expressiveness of Deep Learning
Haskell's Show-Class in Isabelle/HOL
Much Ado About Two
The Sunflower Lemma of Erdős and Rado
Menger's Theorem
Compositional Security-Preserving Refinement for Concurrent Imperative Programs
Arithmetic progressions and relative primes
Transitive closure according to Roy-Floyd-Warshall
Pushdown Systems
Logging-independent Message Anonymity in the Relational Method
Stone Algebras
A Meta-Model for the Isabelle API
Jive Data and Store Model
Greibach Normal Form
A Preprocessor for Linear Diophantine Equalities and Inequalities
Verifying Fault-Tolerant Distributed Algorithms in the Heard-Of Model
Foundation of geometry in planes, and some complements: Excluding the parallel axioms
With-Type - Poor man's dependent types
CRYSTALS-Kyber
The Polylogarithm Function
Landau Symbols
Birkhoff's Representation Theorem For Finite Distributive Lattices
Relational Forests
A framework for establishing Strong Eventual Consistency for Conflict-free Replicated Datatypes
Relational Characterisations of Paths
Certification Monads
AutoFocus Stream Processing for Single-Clocking and Multi-Clocking Semantics
Normalization by Evaluation
The Halting Problem is Soluble in Malament-Hogarth Spacetimes
HOLCF-Prelude
The pi-calculus in nominal logic
Ceva's Theorem
Markov Decision Processes with Rewards
A Fast SAT Solver for Isabelle in Standard ML
Parallel Shear Sort
Closest Pair of Points Algorithms
Formalizing Push-Relabel Algorithms
A data flow analysis algorithm for computing dominators
Regular Sets and Expressions
The Independence of the Continuum Hypothesis in Isabelle/ZF
A Correctness Proof for the Volpano/Smith Security Typing System
Fundamental Properties of Valuation Theory and Hensel's Lemma
Verification of the UpDown Scheme
Lambert Series
Kleene Algebra
VCG - Combinatorial Vickrey-Clarke-Groves Auctions
Verified SAT-Based AI Planning
The Stone-Cech Compactification
Binary codes that do not preserve primitivity
Orbit-Stabiliser Theorem with Application to Rotational Symmetries
Elimination of Repeated Factors Algorithm
The Tensor Product on Hilbert Spaces
Interval Temporal Logic on Natural Numbers
Formalization of Multiway-Join Algorithms
Mission-time Linear Temporal Logic
The CHSH inequality: Tsirelson's upper-bound and other results
Applicative Lifting
Pratt's Primality Certificates
Parameterized Dynamic Tables
Probabilistic Primality Testing
Lattice Properties
A Generic Framework for Verified Compilers
A Formal CHERI-C Memory Model
Gray Codes for Arbitrary Numeral Systems
An Abstract Formalization of Gödel's Incompleteness Theorems
The Myhill-Nerode Theorem Based on Regular Expressions
Expected Shape of Random Binary Search Trees
Cardinality and Representation of Stone Relation Algebras
The Hereditarily Finite Sets
The Unified Policy Framework (UPF)
Algebras for Iteration, Infinite Executions and Correctness of Sequential Computations
The Generalized Multiset Ordering is NP-Complete
Operational Semantics formally proven in HOL-CSP
Interpolation Polynomials (in HOL-Algebra)
A Definitional Encoding of TLA* in Isabelle/HOL
Proving the Impossibility of Trisecting an Angle and Doubling the Cube
Regular Tree Relations
Maximum Segment Sum
Metatheory of Q0
Functional Automata
A Sequential Imperative Programming Language Syntax, Semantics, Hoare Logics and Verification Environment
Priority Queues Based on Braun Trees
Monadification, Memoization and Dynamic Programming
Paraconsistency
Ramsey's theorem, infinitary version
The Karatsuba Square Root Algorithm
Shallow Expressions
Doob's Upcrossing Inequality and Martingale Convergence Theorem
A Formalization of Knuth-Bendix Orders
Clique is not solvable by monotone circuits of polynomial size
Young's Inequality for Increasing Functions
Randomised Social Choice Theory
A Hoare Logic for Diverging Programs
Free Boolean Algebra
Verified Construction of Static Single Assignment Form
Inductive Study of Confidentiality
Partial Correctness of the Top-Down Solver
Symmetric Polynomials
Transition Systems and Automata
Quantum and Classical Registers
Formalised Burrows-Wheeler Transform
Enumeration of Equivalence Relations
Positional Notation for Natural Numbers in an Arbitrary Base
Formal Verification of Modern SAT Solvers
The Schwartz-Zippel Lemma
Dyck Language
Liouville numbers
A formalisation of the Cocke-Younger-Kasami algorithm
First-Order Theory of Rewriting
Making Arbitrary Relational Calculus Queries Safe-Range
p-adic Fields and p-adic Semialgebraic Sets
An Efficient Generalization of Counting Sort for Large, possibly Infinite Key Ranges
Tree Decomposition
Formalization of Refinement Calculus for Reactive Systems
Featherweight OCL: A Proposal for a Machine-Checked Formal Semantics for OCL 2.5
Sauer-Shelah Lemma
Hardness of Lattice Problems
Region Quadtrees
Formal Puiseux Series
van Emde Boas Trees
The Hales-Jewett Theorem
Relaxing Safely: Verified On-the-Fly Garbage Collection for x86-TSO
Derangements Formula
Zermelo Fraenkel Set Theory in Higher-Order Logic
The Transcendence of π
The Weak Spectroscopy Game to Characterize Behavioral Equivalences
Groups, Rings and Modules
Definitive Set Semantics for LTL3
Basic Geometric Properties of Triangles
Verifying a Decision Procedure for Pattern Completeness
Cauchy's Mean Theorem and the Cauchy-Schwarz Inequality
Integration theory and random variables
Aristotle's Assertoric Syllogistic
The Worker/Wrapper Transformation
Finite Automata in Hereditarily Finite Set Theory
Subresultants
No Faster-Than-Light Observers
Labeled Transition Systems
Upper Bounding Diameters of State Spaces of Factored Transition Systems
A Combinator Library for Prefix-Free Codes
A Codatatype of Formal Languages
Group Law of Edwards Elliptic Curves
Separation Algebra
Gromov Hyperbolicity
Three Squares Theorem
Tensor Product of Matrices
Type Constructor Classes and Monad Transformers
A Verified Functional Implementation of Bachmair and Ganzinger's Ordered Resolution Prover
The Sum-of-Squares Function and Jacobi's Two-Square Theorem
Digit Expansions
Stochastic Matrices and the Perron-Frobenius Theorem
The Sumcheck Protocol
First-Order Logic According to Harrison
IDE: Introduction, Destruction, Elimination
A Formalization of Strong Security
Auto2 Prover
The CAVA Automata Library
Schutz' Independent Axioms for Minkowski Spacetime
Hall's Marriage Theorem
Cofinality and the Delta System Lemma
A Verified Code Generator from Isabelle/HOL to CakeML
Simplicial Complexes and Boolean functions
Implementing field extensions of the form Q[sqrt(b)]
A Probabilistic Proof of the Girth-Chromatic Number Theorem
Converting Linear Temporal Logic to Deterministic (Generalised) Rabin Automata
Homogeneous Linear Diophantine Equations
pGCL for Isabelle
Proof Strategy Language
Derivatives of Logical Formulas
Sorted Terms
Compactness Theorem for Propositional Logic and Combinatorial Applications
Ackermann's Function Is Not Primitive Recursive
Conservation of CSP Noninterference Security under Sequential Composition
Relational Divisibility
The Jordan-Hölder Theorem
The Hahn and Jordan Decomposition Theorems
Verification Components for Hybrid Systems
Types, Tableaus and Gödel's God in Isabelle/HOL
Relational Minimum Spanning Tree Algorithms
Pólya's Proof of the Weighted Arithmetic-Geometric Mean Inequality
Synthetic Completeness
Mission-time Linear Temporal Logic to Regular Expressions
Formalization of CommCSL: A Relational Concurrent Separation Logic for Proving Information Flow Security in Concurrent Programs
Restriction Spaces: a Fixed-Point Theory
Stewart's Theorem and Apollonius' Theorem
Median Method
The Incompatibility of Fishburn-Strategyproofness and Pareto-Efficiency
Boolean Expression Checkers
From THE BOOK: Two Squares via Involutions
The string search algorithm by Knuth, Morris and Pratt
Information Flow Noninterference via Slicing
The Textbook Proof of Huffman's Algorithm
Concurrent Refinement Algebra and Rely Quotients
Axiom Systems for Category Theory in Free Logic
Büchi Complementation
Chamber Complexes, Coxeter Systems, and Buildings
A Sequent Calculus for First-Order Logic
NREST: Nondeterministc RESult monad with Time
Efficient Mergesort
Backing up Slicing: Verifying the Interprocedural Two-Phase Horwitz-Reps-Binkley Slicer
Combinatorics on Words Basics
Szpilrajn Extension Theorem
From Abstract to Concrete Gödel's Incompleteness Theorems - Part I
Verified Complete Test Strategies for Finite State Machines
The Hurwitz and Riemann ζ Functions
Probabilistic Noninterference
The Balog-Szemerédi-Gowers Theorem
Arrow and Gibbard-Satterthwaite
Transformer Semantics
Formalisation of an Adaptive State Counting Algorithm
Lie Groups and Algebras
Rely-Guarantee Extensions and Locks
Khovanskii's Theorem
A Theory of Architectural Design Patterns
Two algorithms based on modular arithmetic: lattice basis reduction and Hermite normal form computation
Computational p-Adics
SHA1, RSA, PSS and more
Syntax and semantics of a GPU kernel programming language
Kruskal's Algorithm for Minimum Spanning Forest
Farey Sequences and Ford Circles
An Isabelle/HOL Formalization of the Modular Assembly Kit for Security Properties
Language Partitioning for Mission-time Linear Temporal Logic
The Median-of-Medians Selection Algorithm
Iptables_Semantics
Muntac: A Verified Certificate Checker for Timed Automata
Minkowski's Theorem
Elementary Graph Traversal Algorithms
Monoidal Categories
Developing Security Protocols by Refinement
Solving Cubic and Quartic Equations
Cardinality of Equivalence Relations
The IMAP CmRDT
Completeness theorem
Two theorems about the geometry of the critical points of a complex polynomial
Prime Number Theorem with Remainder Term
A Proof of Hilbert Basis Theorem and an Extension to Formal Power Series
Regular Algebras
List Index
The Partition Function and the Pentagonal Number Theorem
Automated Stateful Protocol Verification
Probabilistic while loop
Quantum Hoare Logic
The Poincaré-Bendixson Theorem
A meta-modal logic for bisimulations
A Generalization of the Cauchy-Davenport theorem
Properties of Orderings and Lattices
Lazy Lists II
Topological semantics for paraconsistent and paracomplete logics
Category Theory with Adjunctions and Limits
An Incremental Simplex Algorithm with Unsatisfiable Core Generation
Verification of the Deutsch-Schorr-Waite Graph Marking Algorithm using Data Refinement
Fun With Functions
Stream Processing Components: Isabelle/HOL Formalisation and Case Studies
Differential Game Logic
Infinite Lists
Zippy - Generic White-Box Proof Search with Zippers
Verified Algorithms for Solving Markov Decision Processes
CRYSTALS-Kyber_Security
Abstract Soundness
Multi-Head Monitoring of Metric Dynamic Logic
A Verified Imperative Implementation of B-Trees
CSP Semantics over Restriction Spaces
Decreasing Diagrams
Matrices, Jordan Normal Forms, and Spectral Radius Theory
Free Groups
Implementing the Goodstein Function in λ-Calculus
Disintegration Theorem
The Safely Composable DOM
Formalization of Recursive Path Orders for Lambda-Free Higher-Order Terms
Number Theoretic Transform
Soundness and Completeness of an Axiomatic System for First-Order Logic
General Probabilistic Techniques for Combinatorics and the Lovasz Local Lemma
The Safety of Call Arity
MLSS Decision Procedure
Parikh's Theorem
HOL-CSPM - Architectural operators for HOL-CSP
A Shorter Compiler Correctness Proof for Language IMP
Isabelle/C
Finitely Generated Abelian Groups
Putting the 'K' into Bird's derivation of Knuth-Morris-Pratt string matching
An Efficient Normalisation Procedure for Linear Temporal Logic: Isabelle/HOL Formalisation
Locally Nameless Sigma Calculus
Unification Utilities for Isabelle/ML
Automation of Boolos' Curious Inference in Isabelle/HOL
Ptolemy's Theorem
Mutually Recursive Partial Functions
Executable Transitive Closures of Finite Relations
Definition and Elementary Properties of Ultrametric Spaces
POPLmark Challenge Via de Bruijn Indices
Cardinality of Multisets
Some classical results in inductive inference of recursive functions
Verified Metatheory and Type Inference for a Name-Carrying Simply-Typed Lambda Calculus
Differential Dynamic Logic
Taylor Models
An Exponential Improvement for Diagonal Ramsey
Formal Specification of a Generic Separation Kernel
A Verified Efficient Implementation of the Weighted Path Order
The meta theory of the Incredible Proof Machine
Flow Networks and the Min-Cut-Max-Flow Theorem
Worklist Algorithms
ABY3 Multiplication and Array Shuffling
Strong Normalization of Moggis's Computational Metalanguage
A Sound and Complete Calculus for Probability Inequalities
A Theory of Featherweight Java in Isabelle/HOL
ConcurrentHOL
Reasoning about Lists via List Interleaving
Lehmer's Theorem
LOFT - Verified Migration of Linux Firewalls to SDN
Difference Bound Matrices
No Faster-Than-Light Observers (GenRel)
Bertrand's postulate
Selected Problems from the International Mathematical Olympiad 2019
The Cardinality of the Continuum
A Case Study in Basic Algebra
Communicating Concurrent Kleene Algebra for Distributed Systems Specification
Deep Embedding of Intuitionistic Linear Logic
Perfect Fields
MiniSail - A kernel language for the ISA specification language SAIL
Quantum projective measurements and the CHSH inequality
Countable Ordinals
Formalization of (Conflict-)Serializability and Strict Two-Phase Locking
The LambdaMu-calculus
Quantum Fourier Transform
Inference of Extended Finite State Machines
Perron-Frobenius Theorem for Spectral Radius Analysis
File Refinement
Pop-Refinement
A shallow embedding of HyperCTL
Polynomial Factorization
A Variant of the Superposition Calculus
Verified Efficient Implementation of Gabow's Strongly Connected Components Algorithm
Lower Semicontinuous Functions
The Relational Method with Message Anonymity for the Verification of Cryptographic Protocols
Proving the Correctness of Disk Paxos
Conformance Relations between Input/Output Languages
Transitive Models of Fragments of ZFC
Cardinality of Set Partitions
Network Security Policy Verification
A Formal Development of a Polychronous Polytimed Coordination Language
Catoids, Categories, Groupoids
First-Order Logic According to Fitting
A Formal Model of the Document Object Model
Spivey's Generalized Recurrence for Bell Numbers
The Hidden Number Problem
Program Construction and Verification Components Based on Kleene Algebra
Graph Saturation
The Sigmoid Function and the Universal Approximation Theorem
Irrationality Criteria for Series by Erdős and Straus
A Compositional and Unified Translation of LTL into ω-Automata
Propositional Resolution and Prime Implicates Generation
Lazifying case constants
Formal Proof of Dilworth's Theorem
Secondary Sylow Theorems
Hyperdual Numbers and Forward Differentiation
Bernoulli Numbers
Z Mathematical Toolkit in Isabelle/HOL
The General Triangle Is Unique
The number of comparisons in QuickSort
Weight-Balanced Trees
Octonions
Loop freedom of the (untimed) AODV routing protocol
The Nash-Williams Partition Theorem
Constructive Cryptography in HOL: the Communication Modeling Aspect
A General Method for the Proof of Theorems on Tail-recursive Functions
The Kuratowski Closure-Complement Theorem
Dynamic and robust timetable rescheduling for uncertain railway disruptions
A data-driven bi-objective matheuristic for energy-optimising timetables in a passenger railway network
Computational decision-support for railway traffic management and associated configuration challenges: An experimental study
Optimization of handouts for rolling stock rotations
Optimization of urban rail transit station spacing for minimizing passenger travel time
Stability analysis of railway dispatching plans in a stochastic and dynamic environment
Secure rail station - Research on the effect of security checks on passenger flow
A modelling and simulation study of a metro line as a time-delayed switched system
GIS and genetic algorithm based integrated optimization for rail transit system planning
Improving railway performance in Norway
Energy-saving train scheduling diagram for automatically operated electric railway
Optimal multi-class rescheduling of railway traffic
Improvement of timetable robustness by analysis of drivers' operation based on decision trees
Shippers/freight forwarders' acceptance of dedicated rail freight corridors for freight mobility in India
Dimensioning windows for railway infrastructure maintenance: Cost efficiency versus traffic impact
A study of homogeneity of operating programs on operation quality considering the occupancy of infrastructure
A tool for the rapid selection of a railway signalling strategy to implement train control optimisation for energy saving
Does the incumbent have an advantage in open access passenger rail competition? A case study on the Prague-Brno line
Predicting and mitigating small fluctuations in station dwell times
Railway line capacity utilisation and its impact on maintenance costs
Guest editorial to the special issue of the best papers of RailBeijing 2021
What employees do today because of their experience yesterday: Previous exposure to yellow: number aspects as a cause for SPAD incidents
A simulation model for evaluating facilities' adaptability in the fare collection area of subway stations
Competition for and in the passenger rail market: Comparing open access versus franchised train operators' costs and reliability in Britain
Enhancing international rail transportation
Optimization of sea-rail intermodal container collection and distribution under novel port layout
Exploring the relationship between the determinants and the ridership decrease of urban rail transit station during the COVID-19 pandemic incorporating spatial heterogeneity
A new operations approach for Bangkok Metro Green Line using short turn operation patterns
Quality in rail timetabling - A detailed review of stakeholders' interests compared with current practices in Germany
Towards a comprehensive model for track allocation and roll-time scheduling at marshalling yards
Semi-quantitative risk assessment of adjacent track accidents on shared-use rail corridors
Railway capacity: A review of analysis methods
The load planning and sequencing problem for double-stack trains
Conflict-free railway track assignment at depots
Perceived service quality based on passenger and trip characteristics: A structural equation modeling approach
Microscopic simulation of decentralized dispatching strategies in railways
Capacity analysis of railway lines in Germany - A rigorous discussion of the queueing based approach
A reinforcement learning approach to solving very-short term train rescheduling problem for a single-track rail corridor
Determination of passenger train reliability through travel delay
An evaluation of the fairness of railway timetable rescheduling in the presence of competition between train operators
Relationship between built environment characteristics of TOD and subway ridership: A causal inference and regression analysis of the Beijing subway
The enablers and inhibitors of intermodal rail freight between Asia and Europe
Dynamic pricing for passenger groups of high-speed rail transportation
Timetable optimization for a moving block system
Maintenance scheduling within rolling stock planning in railway operations under uncertain maintenance durations
Train dwell time models for crowded metro stations using a bivariate distribution function
Optimizing and synchronizing timetable in an urban subway network with stop-skip strategy
A MILP model to improve the robustness of a railway timetable by retiming and rerouting in a complex bottleneck area
Use of mobile phone data for analysis of number of train travellers
Vehicle-to-Grid (V2G) as line-side energy storage for support of DC-powered electric railway systems
Optimal running time supplement distribution in train schedules for energy-efficient train control
The evaluation of competition effect on rail fares using the difference-in-difference method through symmetric and lagged spans
Modelling and analysis of Virtual Coupling with dynamic safety margin considering risk factors in railway operations
Identification of causal scenarios and application of leading indicators in the interconnection mode of urban rail transit based on STPA
Modeling train route decisions during track works
System train paths as key to efficient infrastructure usage for on-track competition in ITF-regimes