researchr - search publication proof assistant

researchr

You are not signed in
Sign in
Sign up

178 publication results matching 'proof assistant'

A Declarative Language for the Coq Proof Assistant
… This paper presents a new proof language for the Coq proof assistant. This language uses the declarative style. It aims at providing a simple, natural …. We explain how this language can be used to implement formal proof sketches …
Pierre Corbineau. TYPES 2008: 69-84 [doi]
Defining and Reasoning About Recursive Functions: A Practical Tool for the Coq Proof Assistant
… We present a practical tool for defining and proving properties of recursive functions in the Coq proof assistant. The tool proceeds by generating from pseudo-code (Coq functions that need not be total nor terminating) the graph …
Gilles Barthe, Julien Forest, David Pichardie, Vlad Rusu. FLOPS 2006: 114-129 [doi]
Web Interfaces for Proof AssistantsENTCS, 174(2):49-61, 2007. [doi]
The Twelf Proof AssistantCarsten SchÃ¼rmann. tphol 2009: 79-83 [doi]
Crafting a Proof AssistantAndrea Asperti, Claudio Sacerdoti Coen, Enrico Tassi, Stefano Zacchiroli. TYPES 2007: 18-32 [doi]
A Proof Assistant for PSFSjouke Mauw, Gert J. Veltink. cav 1992: 158-168
Algebraic Proof Assistants in HOLRix Groenboom, Chris Hendriks, Indra Polak, Jan Terlouw, Jan Tijmen Udding. mpc 1995: 304-321
Design Proof Assistant (Abstract)Gérard P. Huet. RTA 1996: 153
A Proof Assistant for Mobile ProcessesXutao Du, Zhoujun Li. appt 2003: 204-214 [doi]
Equality in computer proof-assistantsAdam Grabowski, Artur Kornilowicz, Christoph Schwarzweller. FedCSIS 2015: 45-54 [doi]
A Proof Assistant for Alloy SpecificationsMattias Ulbrich, Ulrich Geilmann, Aboubakr Achraf El Ghazi, Mana Taghdiri. TACAS 2012: 422-436 [doi]
Growing a proof assistantBowman, William J. Higher-Order Programming with Effects, 65, 2016.
CCS used as a proof-assistant toolChau Chun Hung. pstv 1985: 387-398
Proving Self-Stabilization with a Proof AssistantPierre Courtieu. ipps 2002: [doi]
Isabelle as Document-Oriented Proof AssistantMakarius Wenzel. mkm 2011: 244-259 [doi]
Towards formalising AADL in Proof AssistantsJean-Paul Bodeveix, David Chemouil, Mamoun Filali, Martin Strecker. ENTCS, 141(3):153-169, 2005. [doi]
User Interaction with the Matita Proof AssistantAndrea Asperti, Claudio Sacerdoti Coen, Enrico Tassi, Stefano Zacchiroli. JAR, 39(2):109-139, 2007. [doi]
Types with semantics: soundness proof assistantOlha Shkaravska. ICFP 2005: 50-57 [doi]
External Rewriting for Skeptical Proof AssistantsQuang Huy Nguyen, Claude Kirchner, Hélène Kirchner. JAR, 29(3-4):309-336, 2002.
Mathematical Libraries as Proof Assistant EnvironmentsClaudio Sacerdoti Coen. mkm 2004: 332-346 [doi]

Sign in or sign up to see more results.

runs on WebDSL