yusuke1997/dblp-id-title huggingface dataset:
Towards anatomical modelling of multiple organs interaction using real time GPU based non-linear elasticity
Conductometric Catheter-Mounted Pressure Sensor
Examination of Muscle Effort and Fatigue During Virtual and Actual Laparoscopic Surgical Skills Practice
Gunner Goggles: Implementing Augmented Reality into Medical Education
Evaluating Tool-Artery Interaction Force during Endovascular Neurosurgery for Developing Haptic Engine
Constrained Point-Based Framework with Efficient Mechanical Interaction for Virtual Surgery
Validating Metrics for a Mastoidectomy Simulator
Direct versus Indirect Laryngoscopic Visualization in Human Endotracheal Intubation: A Tool for Virtual Anesthesia Practice and Teleanesthesiology
Volume Visual Attention Maps (VVAM) in Ray-Casting Rendering
Initial Implementation of Mixed Reality Simulation Targeting Teamwork and Patient Safety
The Validation of an Instrumented Simulator for the Assessment of Performance and Outcome of Knot Tying Skill: A Pilot Study
A Novel Automated Drug Simulant Recognition System for Naturalistic Real-Time Medical Simulation
Development of a Tele-Anesthesia Preoperative Clinic to Support Distant Military Treatment Facilities for the European Regional Medical Command
Surgical Tools Recognition and Pupil Segmentation for Cataract Surgical Process Modeling
Guidewire and Catheter Behavioural Simulation
Learning & Retention in Adaptive Serious Games
Haptic Feedback for Multilayer Cutting
Natural Orifice Transluminal Endoscopic Surgery (NOTES): An Opportunity for Augmented Reality Guidance
Quantizing the Void: Extending Web3D for Space-Filling Haptic Meshes
3D++ Visualisation of MEBN Graphs and Screen Representations of Patient Models (PIXIE II)
Real-Time Ultrasound Simulation for Training of US-Guided Needle Insertion in Breathing Virtual Patients
The Impact of Secondary-Task Type on the Sensitivity of Reaction-Time Based Measurement of Cognitive Load for Novices Learning Surgical Skills Using Simulation
Burrhole Simulation for an Intracranial Hematoma Simulator
A Unified Framework for Haptic Interaction in Multimodal Virtual Environments
Development of a Soft Tissue Elastography Robotic Arm (STiERA)
Virtual Reality and Haptic Interface for Cellular Injection Simulation
Pupil Response to Precision in Surgical Task Execution
A Concept for Overlaid-Type Surgical Navigation System with Organ Modification Functions Using Non-Contact Type Surface Measurement
Localized Virtual Patient Model for Regional Anesthesia Simulation Training System
An Integrated Movement Capture and Control Platform Applied Towards Autonomous Movements of Surgical Robots
Objective Structured Clinical Interview Training using a Virtual Human Patient
Endotracheal Intubation with a Traditional Videolaryngoscope Blade versus an Integrated Suction Blade in a Hemorrhagic Airway Cadaver Model
Effects on Performance of Individual versus Dyadic Practice during an Avatar-Based Three-Dimensional Virtual Home Safety Simulation
Development of a Web-Based 3D Module for Enhanced Neuroanatomy Education
Collaborative Engineering: 3-D Optical Imaging and Gas Exchange Simulation of In-Vitro Alveolar Constructs
Virtual Help for Real Surgery: The Case of Awake Surgery
Task Sequencing Effects for Open and Closed Loop Laparoscopic Skills
Deformation-based Augmented Reality for Hepatic Surgery
A Virtual Reality Game for Chronic Pain Management: A Randomized, Controlled Clinical Study
Design for Functional Occlusal Surface of CAD/CAM Crown Using VR Articulator
A Survey of Simulators for Palpation Training
GPU Accelerated Viscous-fluid Deformable Registration for Radiotherapy
Smooth Haptic Interaction from Discontinuous Simulation Data
Expansion of a VR Exposure Therapy System for Combat-Related PTSD to Medics/Corpsman and Persons Following Military Sexual Trauma
An Overview of 3D Video Transmission and Display Technologies for Telemedicine Applications
Training and Assessment of Procedural Skills in Context using an Integrated Procedural Performance Instrument (IPPI)
Haptic Guided Laparoscopy Simulation Improves Learning Curve
Use of Simulation to Understand the Effects of Task Complexity and Time Away on Clinical Confidence
A Comparative Study of Monoscopic and Stereoscopic Display for a Probe-Positioning Task
An Aneurysm Clipping Training Module for the Neurosurgical Training Simulator NeuroSim
Cost Effective Ultrasound Imaging Training Mentor for Use in Developing Countries
Real-Time Simulation of Interaction between Colon and Endoscope for the Colonoscopy Simulation
Stereo Image-Based Arm Tracking for In Vivo Surgical Robotics
A Real-time Knot Detection Algorithm for Suturing Simulation
Ergonomic Usability Testing of Operating Room Devices
Reducing Clinical Trial Costs by Detecting and Measuring the Placebo Effect and Treatment Effect Using Brain Imaging
Medical Documentation Using a Gaze-Driven Camera
Haptics-Constrained Motion for Surgical Intervention
A Study About Coefficients to Estimate the Error in Biomechanical Models Used to Virtually Simulate the Organ Behaviors
Why You Really Eat? Virtual Reality in the Treatment of Obese Emotional Eaters
A Design for Simulating and Validating the Nuss Procedure for the Minimally Invasive Correction of Pectus Excavatum
Eye Gaze Tracking for Endoscopic Camera Positioning: An Application of a Hardware/Software Interface Developed to Automate Aesop
Tele-Control of an Endoscopic Surgical Robot System between Japan and Thailand for Tele-NOTES
Investigation into the Effectiveness of Vibrotactile Feedback to Improve the Haptic Realism of an Arthroscopy Training Simulator
Improving Fiberoptic Intubation with a Novel Tongue Retraction Device
Verifying the Effectiveness of a Computer-Aided Navigation System for Arthroscopic Hip Surgery
Automatic Behavior Analysis During a Clinical Interview with a Virtual Human
The Effect of Haptic Degrees of Freedom on Task Performance in Virtual Surgical Environments
Patient Specific Surgical Simulator for the Evaluation of the Movability of Bimanual Robotic Arms
Haptic Simulation of the Liver with Respiratory Motion
A Multi-Layered Needle Injection Simulator
Development of a Generic Tubular Tree Structure for the Modeling of Orbital Cranial Nerves
Virtual Reality Paced Serial Assessment Test for Neuropsychological Assessment of a Military Cohort
Hierarchical Task Analysis of Hybrid Rigid Scope Natural Orifice Translumenal Endoscopic Surgery (NOTES) Cholecystectomy Procedures
Real-Time Complex Cognitive Surgical Simulator with Testing
Do Not Forget the Oldest Old: Design Principles for the 80+
The Development of a Haptic Interface for the Virtual Translumenal Endoscopic Surgical Trainer (VTEST TM )
Performance Optimization of Web-Based Medical Simulation
Virtual Endoscopy on a Portable Navigation System for ENT Surgery
Virtual Open Heart Surgery Segmentation
A Virtual Reality Simulator for Training of Needle Biopsy of Thyroid Gland Nodules
Use of Clinical Simulations for Patient Education: Targeting an Untapped Audience
A Prototype Stimulator System for Noninvasive Low Intensity Focused Ultrasound Delivery
Towards THz Medical Imaging; Reflective Imaging of Animal Tissues
A Machine Learning-Based Scalable Approach For Real-Time Surgery Simulation
Developing and Evaluating Virtual Cardiotomy for Preoperative Planning in Congenital Heart Disease
Computed Tomography as Ground Truth for Stereo Vision Measurements of Skin
Toward a Simulation and Assessment Method for the Practice of Camera-Guided Rigid Bronchoscopy
Potential of the Navigated Controlled Surgery at the Lateral Skull Base with the Navigated Control Unit (NCU 2.0)
Pneumoperitoneum Technique Simulation in Laparoscopic Surgery on Lamb Liver Samples and 3D Reconstruction
A Simulation Framework for Tool Tissue Interactions in Robotic Surgery
Development of a Minimally Invasive Implantable Wireless Vital Signs Sensor Platform
Particle Based Simulation of the Aortic Valve by Considering Heart's Pulsation
Design of a Low Cost Multiple User Virtual Environment for Rehabilitation (MUVER) of Patients with Stroke
Avoiding Focus Shifts in Surgical Telementoring Using an Augmented Reality Transparent Display
3D Measuring Tool for Estimating Femoroacetabular Impingement
A Demonstration of the Storz C-CAM in Endoscopic Imagery Projection for Far Forward Battlefield Telemetric Support and Training
An Interactive Program to Conceptualize the Anatomy of the Internal Brainstem in 3D
Simulation of Osteotomy and Support for Surgery using VR Haptic Device
Implementing Virtual Worlds for Systematic Training of prehospital CPR in Medical School
Combined Intubation Training (Simulated and Human) for 4 th Year Medical Students: The Center for Advanced Technology and Telemedicine Airway Training Program
3D Physics-Based Registration of 2D Dynamic MRI Data
Requirement Specification for Surgical Simulation Systems with Surgical Workflows
The Initiation of a Preoperative and Postoperative Telemedicine Urology Clinic
Computer Imagery and Neurological Rehabilitation: On the Use of Augmented Reality in Sensorimotor Training to Step Up Naturally Occurring Cortical Reorganization in Patients Following Stroke
Evaluation of Tensiometric Assessment as a Measure of Skill Degradation
A New Part Task Trainer for Teaching and Learning Confirmation of Endotracheal Intubation
Evaluation of RGP Contact Lens Fitting in Keratoconus Patients Using Hierarchical Fuzzy Model and Genetic Algorithms
Toward a Comprehensive Hybrid Physical-Virtual Reality Simulator of Peripheral Anesthesia with Ultrasound and Neurostimulator Guidance
Development of a Tele ENT Program to Support Distant Military Treatment Facilities for the European Regional Medical Command
In Vivo Robotics for Natural Orifice Transgastric Peritoneoscopy
Comparative Visualization of Human Nasal Airflows
Liver Pathology Simulation: Algorithm for Haptic Rendering and Force Maps for Palpation Assessment
Gradient-Free Visualization with Multiple Light Approximations
Classification of Restrictive and Obstructive Pulmonary Diseases Using Spirometry Data
A Portable Palpation Training Platform with Virtual Human Patient
Raven Surgical Robot Training in Preparation for da Vinci ® Use: A Randomized Prospective Trial
Manual registration of ultrasound with CT/Planning data for hepatic surgery
Design and Implementation of a Visual and Haptic Simulator in a Platform for a TEL System in Percutaneuos Orthopedic Surgery
A Resource Management Tool for Real-Time Multimodal Surgical Simulation
Medicine Meets Virtual Reality 19 - NextMed, MMVR 2012, Newport Beach, California, USA, February 9-11, 2012
Comprehensive 3D Visual Simulation for Radiation Therapy Planning
Virtual Gait Training for Children with Cerebral Palsy using the Lokomat Gait Orthosis
Objective Surgical Performance Assessment for Virtual Hysteroscopy
Computational Modeling of Human Head Electromagnetics for Source Localization of Milliscale Brain Dynamics
A Virtual Reality Throat Examination Simulation
Real-Time Human Pose Detection and Tracking for Tele-Rehabilitation in Virtual Reality
A Simulator to Explore the Role of Haptic Feedback in Cataract Surgery Training
A Bloodstream Simulation Based on Particle Method
Simulation of Vaginal Wall Biomechanical Properties from Pelvic Floor Closure Forces Map
Virtual Airway Skills Trainer (VAST) Simulator
Modeling the Thermal Effect of the Bipolar Electrocautery for Neurosurgery Simulation
Use of a Linear Motion Stroke Potentiometer As a High Precision Sensor for Linear Translation in a Laparoscopic Ligating Loop Simulation
Interactive Physically-based X-ray Simulation: CPU or GPU?
Computer Simulation of Corticospinal Activity during Transcranial Electrical Stimulation in Neurosurgery
Development of Extracorporeal Suturing Simulation in Virtual Basic Laparoscopic Skill Trainer (VBLaST © )
Application of a New Adaptable Thyroid Model for Ultrasound and Hands-On Skill Assessment
Hip Motion Analysis Using Multi Phase (Virtual and Physical) Simulation of the Patient-specific Hip Joint Dynamics
EYESi Ophthalmoscope - A Simulator for Indirect Ophthalmoscopic Examinations
Simulation of a Human Circulatory System
A Modular Simulation Framework for Colonoscopy using a New Haptic Device
Data Types as Quotients of Polynomial Functors
Interactive and Automated Proofs in Modal Separation Logic (Invited Talk)
A Comprehensive Overview of the Lebesgue Differentiation Theorem in Coq
Relational Parametricity and Quotient Preservation for Modular (Co)datatypes
WorkingWiki: a MediaWiki-based platform for collaborative research
Interactive Theorem Proving, First International Conference, ITP 2010, Edinburgh, UK, July 11-14, 2010. Proceedings
A Formalisation of Consistent Consequence for Boolean Equation Systems
Data Refinement in Isabelle/HOL
Autosubst: On Mechanising Binders in a General-Purpose Proof Assistant (Invited Talk)
Adjustable References
Synthetic Kolmogorov Complexity in Coq
The Picard Algorithm for Ordinary Differential Equations in Coq
Validating QBF Validity in HOL4
Formal Reasoning about Classified Markov Chains in HOL
Higher-Order Tarski Grothendieck as a Foundation for Formal Proof
Hypermap Specification and Certified Linked Implementation Using Orbits
Proof of OS Scheduling Behavior in the Presence of Interrupt-Induced Concurrency
Slice Nondeterminism
A Certified Denotational Abstract Interpreter
Generic Authenticated Data Structures, Formally
A Framework for Formal Verification of Compiler Optimizations
A Formalization of the General Theory of Quaternions
Kleene Algebra with Tests and Coq Tools for while Programs
A Verified Earley Parser
Complete Non-Orders and Fixed Points
Reflexive Tactics for Algebra, Revisited
Improved Tool Support for Machine-Code Decompilation in HOL4
Verified Operational Transformation for Trees
A Formalization of the Lévy-Prokhorov Metric in Isabelle/HOL
Proof Pearl: Formalizing Spreads and Packings of the Smallest Projective Space PG(3, 2) Using the Coq Proof Assistant
A machine learning method for real estate operation projects forecasting
Synthetic Undecidability and Incompleteness of First-Order Axiom Systems in Coq
Lem: A Lightweight Tool for Heavyweight Semantics
A Verified and Compositional Translation of LTL to Deterministic Rabin Automata
Automating Formalization by Statistical and Semantic Parsing of Mathematics
Proof Pearl: Constructive Extraction of Cycle Finding Algorithms
Formalizing Algorithmic Bounds in the Query Model in EasyCrypt
A Formalisation of Gallagher's Ergodic Theorem
Machine-Checked Verification of the Correctness and Amortized Complexity of an Efficient Union-Find Implementation
Abstract Interpretation of Annotated Commands
Automated Theory Exploration for Interactive Theorem Proving: - An Introduction to the Hipster System
Construction of Real Algebraic Numbers in Coq
Showing Invariance Compositionally for a Process Algebra for Network Protocols
Refinement to Imperative/HOL
Applying ACL2 to the Formalization of Algebraic Topology: Simplicial Polynomials
How to Get More Out of Your Oracles
The Flow of ODEs
Extending Coq with Imperative Features and Its Application to SAT Verification
"Repressed book: (re)presentation of National Cultural Heritage from the Funds of the Vasyl Stefanyk National Scientific Library of Ukraine in Lviv" - Information Technologies for the Implementation of a Cross-Sectoral Project
A Linear Algebra Wiki
A Verified Runtime for a Verified Theorem Prover
Applying Data Refinement for Monadic Programs to Hopcroft's Algorithm
The Isabelle ENIGMA
Towards Verified Handwritten Calculational Proofs - (Short Paper)
Towards Certified Meta-Programming with Typed Template-Coq
Automatic Functional Correctness Proofs for Functional Search Trees
Rough Diamond: An Extension of Equivalence-Based Rewriting
15th International Conference on Interactive Theorem Proving, ITP 2024, Tbilisi, Georgia, September 9-14, 2024
Formalization of Basic Combinatorics on Words
Synthesis of Distributed Mobile Programs Using Monadic Types in Coq
Automatic Data Refinement
Using Abstract Stobjs in ACL2 to Compute Matrix Normal Forms
Certifying Standard and Stratified Datalog Inference Engines in SSReflect
A Computer-Algebra-Based Formal Proof of the Irrationality of ζ(3)
Tealeaves: Structured Monads for Generic First-Order Abstract Syntax Infrastructure
13th International Conference on Interactive Theorem Proving, ITP 2022, Haifa, Israel, August 7-10, 2022
Formalization of the Fundamental Group in Untyped Set Theory Using Auto2
Intelligent project portfolio development of IT companies
12th International Conference on Interactive Theorem Proving, ITP 2021, Rome, Italy (Virtual Conference), June 29 - July 1, 2021
The PlanetMath Encyclopedia
Nanopass Back-Translation of Call-Return Trees for Mechanized Secure Compilation Proofs
Charge! - A Framework for Higher-Order Separation Logic in Coq
Termination of Isabelle Functions via Termination of Rewriting
First-Order Guarded Coinduction in Coq
Reimplementing Mizar in Rust
Heterogeneous Proofs: Spider Diagrams Meet Higher-Order Provers
Proof Assistants as Teaching Assistants: A View from the Trenches
Formalized Timed Automata
A Proof-Producing Compiler for Blockchain Applications
Redex2Coq: Towards a Theory of Decidability of Redex's Reduction Semantics
Formalized functional analysis with semilinear maps
Bag Equivalence via a Proof-Relevant Membership Relation
Ornaments for Proof Reuse in Coq
On the Formalization of Fourier Transform in Higher-order Logic
Formalizing Ring Theory in PVS
Towards Automating Permutation Proofs in Rocq: A Reflexive Approach with Iterative Deepening Search (Short Paper)
Candle: A Verified Implementation of HOL Light
AUTO2, A Saturation-Based Heuristic Prover for Higher-Order Logic
Equations: A Dependent Pattern-Matching Compiler
Scalable LCF-Style Proof Translation
A Verified Generational Garbage Collector for CakeML
Formalization of the Lindemann-Weierstrass Theorem
Program Optimisations via Hylomorphisms for Extraction of Executable Code
Physical Addressing on Real Hardware in Isabelle/HOL
Conway Normal Form: Bridging Approaches for Comprehensive Formalization of Surreal Numbers
Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder
Formalization of the Resolution Calculus for First-Order Logic
An Elementary Formal Proof of the Group Law on Weierstrass Elliptic Curves in Any Characteristic
Three Chapters of Measure Theory in Isabelle/HOL
Proof Pearl: Faithful Computation and Extraction of μ-Recursive Algorithms in Coq
Formalizing Bounded Increase
More SPASS with Isabelle - Superposition with Hard Sorts and Configurable Simplification
Formalising a Turing-Complete Choreographic Language in Coq
Certified Implementability of Global Multiparty Protocols
Refinement with Time - Refining the Run-Time of Algorithms in Isabelle/HOL
Relational Decomposition
A Coq Formalization of Taylor Models and Power Series for Solving Ordinary Differential Equations
Using Locales to Define a Rely-Guarantee Temporal Logic
What Makes a Mathematician Tick? (Invited Talk)
Automatic Test-Case Reduction in Proof Assistants: A Case Study in Coq
Reification by Parametricity - Fast Setup for Proof by Reflection, in Two Lines of Ltac
Computer-Aided Cryptographic Proofs
Partiality and Recursion in Interactive Theorem Provers, PAR@ITP 2010, Edinburgh, UK, July 15, 2010
Verifying the LTL to Büchi Automata Translation via Very Weak Alternating Automata
Formal Verification of the Empty Hexagon Number
The DPRM Theorem in Isabelle (Short Paper)
An Increasing Need for Formality (Invited Talk)
Automated Machine-Checked Hybrid System Safety Proofs
Subformula Linking as an Interaction Method
Typed Compositional Quantum Computation with Lenses
Foundational Verification of Stateful P4 Packet Processing
A Formal Proof of Cauchy's Residue Theorem
Verified Tail Bounds for Randomized Programs
Binary-Compatible Verification of Filesystems with ACL2
Formalization of a Stochastic Approximation Theorem
A Coq Tactic for Equality Learning in Linear Arithmetic
A Verified Cyclicity Checker: For Theories with Overloaded Constants
The Isabelle Collections Framework
Djinn, Monotonic
Verifying Object-Oriented Programs with Higher-Order Separation Logic in Coq
Project of an Educational Content Evaluation Recommender System
A Formal Library for Elliptic Curves in the Coq Proof Assistant
Foundational Property-Based Testing
POSIX Lexing with Derivatives of Regular Expressions (Proof Pearl)
Formalizing Functions as Processes
Formalizing the Cholesky Factorization Theorem
A New and Formalized Proof of Abstract Completion
Validating Dominator Trees for a Fast, Verified Dominance Test
A Compact Proof of Decidability for Regular Expression Equivalence
Formalizing Almost Development Closed Critical Pairs (Short Paper)
Lean Formalization of Completeness Proof for Coalition Logic with Common Knowledge
The On-Line Encyclopedia of Integer Sequences: From Punched Cards to Wiki in 46 Years (abstract; invited talk)
Shared-Memory Multiprocessing for Interactive Theorem Proving
Formalizing Implicative Algebras in Coq
Formal Proof and Analysis of an Incremental Cycle Detection Algorithm
Characteristic Formulae for Liveness Properties of Non-Terminating CakeML Programs
Asynchronous Processing of Coq Documents: From the Kernel up to the User Interface
Implementing Hash-Consed Structures in Coq
A Formalized Hierarchy of Probabilistic System Types - Proof Pearl
Interactive Theorem Proving - 4th International Conference, ITP 2013, Rennes, France, July 22-26, 2013. Proceedings
Complete Bidirectional Typing for the Calculus of Inductive Constructions
Finiteness of Symbolic Derivatives in Lean
Proof Pearl: Purely Functional, Simple and Efficient Priority Search Trees and Applications to Prim and Dijkstra
Bridging the Gap: Automatic Verified Abstraction of C
Kalas: A Verified, End-To-End Compiler for a Choreographic Language
Counterexample Generation Meets Interactive Theorem Proving: Current Results and Future Opportunities
Formalising Semantics for Expected Running Time of Probabilistic Programs
Tactics and Certificates in Meta Dedukti
A Verified Enclosure for the Lorenz Attractor (Rough Diamond)
Nonlinear regression models for software size estimation of Data Science and Machine Learning Java-applications
Mechanisation of AKS Algorithm: Part 1 - The Main Theorem
Erratum to: Interactive Theorem Proving
Cardinals in Isabelle/HOL
A Mechanized Translation from Higher-Order Logic to Set Theory
The CakeML Project's Quest for Ever Stronger Correctness Theorems (Invited Paper)
Information-Analytical System for Evaluating the Activity of the Scientific-Pedagogical Staff Based on KPIs at Odesa National Maritime University
Formalizing the Edmonds-Karp Algorithm
Directions in ISA Specification
Portfolio project management
Beating the Productivity Checker Using Embedded Languages
Scott's Representation Theorem and the Univalent Karoubi Envelope
An Agda Formalization of Üresin and Dubois' Asynchronous Fixed-Point Theory
Real-Time Double-Ended Queue Verified (Proof Pearl)
HOL Zero's Solutions for Pollack-Inconsistency
Verifying an Efficient Algorithm for Computing Bernoulli Numbers
Software Verification with ITPs Should Use Binary Code Extraction to Reduce the TCB - (Short Paper)
Logical Formalisation and Analysis of the Mifare Classic Card in PVS
16th International Conference on Interactive Theorem Proving, ITP 2025, Reykjavik, Iceland, September 28 - October 1, 2025
Categoricity Results for Second-Order ZF in Dependent Type Theory
Light-Weight Containers for Isabelle: Efficient, Extensible, Nestable
FoCaLiZe and Dedukti to the Rescue for Proof Interoperability
Advances in the Formalization of the Odd Order Theorem
CalcCheck: A Proof Checker for Teaching the "Logical Approach to Discrete Math"
Integrals Within Integrals: A Formalization of the Gagliardo-Nirenberg-Sobolev Inequality
A Formal Analysis of Algorithms for Matroids and Greedoids
Computational Back-And-Forth Arguments in Constructive Type Theory
Composable Discovery Engines for Interactive Theorem Proving
Formalising Szemerédi's Regularity Lemma in Lean
Transfinite Constructions in Classical Type Theory
Formally Verified Approximations of Definite Integrals
Mechanizing Soundness of Off-Policy Evaluation
Formalizing the Ring of Adèles of a Global Field
A Machine-Checked Proof of the Odd Order Theorem