惯性聚合 高效追踪和阅读你感兴趣的博客、新闻、科技资讯
阅读原文 在惯性聚合中打开

推荐订阅源

Microsoft Security Blog
Microsoft Security Blog
Apple Machine Learning Research
Apple Machine Learning Research
美团技术团队
WordPress大学
WordPress大学
酷 壳 – CoolShell
酷 壳 – CoolShell
G
Google Developers Blog
阮一峰的网络日志
阮一峰的网络日志
The Cloudflare Blog
J
Java Code Geeks
Martin Fowler
Martin Fowler
M
MIT News - Artificial intelligence
IT之家
IT之家
博客园 - 三生石上(FineUI控件)
月光博客
月光博客
Google DeepMind News
Google DeepMind News
小众软件
小众软件
V
V2EX
Hugging Face - Blog
Hugging Face - Blog
爱范儿
爱范儿
OSCHINA 社区最新新闻
OSCHINA 社区最新新闻
Jina AI
Jina AI
freeCodeCamp Programming Tutorials: Python, JavaScript, Git & More
腾讯CDC
B
Blog

cs.HC updates on arXiv.org

From Prompt to Service: An SLM-Based Agent Orchestration Gateway for AI-Driven Virtual Worlds What LLMs Must Forget to Teach Effectively: A DIY Approach to Premodern Japanese Language Pedagogy Quantitative Movement Testing: Measuring Patient Movements from a Single Smartphone Video Vision-Language Models Suppress Female Representations Under Ambiguous Input The New Social Image: How AI Competency and AI Proactivity Influence Self- and Peer-Perceptions in the Workplace TUX: Measuring Human--AI Tacit Understanding LLUMI: Improving LLM Writing Assistance for Mental Health Support with Online Community Feedback VideoFDB: Evaluating Full-Duplex Vision-Speech Capabilities in Conversational Agents Label Over Logic? How Source Cues Bias Human Fallacy Judgments More Than LLMs Inform, Coach, Relate, Listen: Auditing LLM Caregiving Support Roles How Coding Agents Fail Their Users: A Large-Scale Analysis of Developer-Agent Misalignment in 20,574 Real-World Sessions MetaRanker: Human-in-the-loop Active Ranking for Metalens Image Quality Analyzing Persona Effects in Generated Explanations from Multimodal LLM Agents in Urban Perception First head-to-head comparison of agentic AI applied to the analysis of simulated data of the Einstein Telescope Granuscore: A Reference-Free Measure of Granularity for Text Analysis and Question Answering The Timing Dependencies of Trust: Speed, Accuracy, and cBCI Neuro-Decoupling in Human-AI Teams Bayesian Distributional Models of Executive Functioning Visual Matters: Connecting Aesthetic Appeal and Production Quality of Photos, Infographics and Data Visualizations to Credibility of Social Media Posts Data-driven Head Motion Generation through Natural Gaze-Head Coordination Agreement Metrics for LLM-as-Judge Evaluation: What to Report and Why Perceptually Lossless Tactile Texture Synthesis with Compact Spectral Envelope Models MambaGaze: Bidirectional Mamba with Explicit Missing Data Modeling for Cognitive Load Assessment from Eye-Gaze Tracking Data CogAdapt: Transferring Clinical ECG Foundation Models to Wearable Cognitive Load Assessment via Lead Adaptation Augmented Analytics and Decision Quality: The Role of Trust among Non-Technical BI Users Faster Completion, Less Learning: Generative AI Reduced Study Time on Math Problems and the Knowledge They Build PaintCopilot: Modeling Painting as Autonomous Artistic Continuation Personality Engineering with AI Agents: A New Methodology for Negotiation Research PULSE: Agentic Investigation with Passive Sensing for Proactive Intervention in Cancer Survivorship Access Timing as Scaffolding: A Reinforcement Learning Approach to GenAI in Education MAPLE: Self-Supervised Learning-Enhanced Nonlinear Dimensionality Reduction for Visual Analysis
Proviola: A Tool for Proof Re-animation
Carst Tankink, Herman Geuvers, James McKinna, Freek Wiedijk · 2010-05-15 · via cs.HC updates on arXiv.org

To improve on existing models of interaction with a proof assistant (PA), in particular for storage and replay of proofs, we in- troduce three related concepts, those of: a proof movie, consisting of frames which record both user input and the corresponding PA response; a camera, which films a user's interactive session with a PA as a movie; and a proviola, which replays a movie frame-by-frame to a third party. In this paper we describe the movie data structure and we discuss a proto- type implementation of the camera and proviola based on the ProofWeb system. ProofWeb uncouples the interaction with a PA via a web- interface (the client) from the actual PA that resides on the server. Our camera films a movie by "listening" to the ProofWeb communication. The first reason for developing movies is to uncouple the reviewing of a formal proof from the PA used to develop it: the movie concept enables users to discuss small code fragments without the need to install the PA or to load a whole library into it. Other advantages include the possibility to develop a separate com- mentary track to discuss or explain the PA interaction. We assert that a combined camera+proviola provides a generic layer between a client (user) and a server (PA). Finally we claim that movies are the right type of data to be stored in an encyclopedia of formalized mathematics, based on our experience in filming the Coq standard library.