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

推荐订阅源

罗磊的独立博客
L
LangChain Blog
aimingoo的专栏
aimingoo的专栏
IT之家
IT之家
B
Blog
博客园_首页
博客园 - 司徒正美
有赞技术团队
有赞技术团队
博客园 - 聂微东
I
InfoQ
美团技术团队
GbyAI
GbyAI
阮一峰的网络日志
阮一峰的网络日志
H
Help Net Security
大猫的无限游戏
大猫的无限游戏
MyScale Blog
MyScale Blog
WordPress大学
WordPress大学
The GitHub Blog
The GitHub Blog
A
About on SuperTechFans
人人都是产品经理
人人都是产品经理
Microsoft Azure Blog
Microsoft Azure Blog
Engineering at Meta
Engineering at Meta
钛媒体:引领未来商业与生活新知
钛媒体:引领未来商业与生活新知
The Cloudflare 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
READ-EVAL-PRINT in Parallel and Asynchronous Proof-checking
Makarius Wenzel · 2013-07-08 · via cs.HC updates on arXiv.org

The LCF tradition of interactive theorem proving, which was started by Milner in the 1970-ies, appears to be tied to the classic READ-EVAL-PRINT-LOOP of sequential and synchronous evaluation of prover commands. We break up this loop and retrofit the read-eval-print phases into a model of parallel and asynchronous proof processing. Thus we explain some key concepts of the Isabelle/Scala approach to prover interaction and integration, and the Isabelle/jEdit Prover IDE as front-end technology. We hope to open up the scientific discussion about non-trivial interaction models for ITP systems again, and help getting other old-school proof assistants on a similar track.