Tag theorem-proving [59 articles] Export

Recent papers classified by the tag theorem-proving.

	Mechanical Reasoning about Families of UTP Theories [My Copy] Electronic Notes in Theoretical Computer Science, Vol. 240 (02 July 2009), pp. 239-257. by Frank Zeyda, Ana Cavalcanti posted to z utp theorem-proving semantics reasoning proof 2009 by michaelbanks on 2009-11-27 14:59:33 as
	An application of co-inductive types in Coq: Verification of the alternating bit protocol [My Copy] Types for Proofs and Programs (1996), pp. 135-152. by Eduardo Giménez posted to verification theorem-proving recursion master-project logic functional-programming coq coinduction by mvermaat on 2009-11-05 14:02:51 as
	Differential Dynamic Logic for Verifying Parametric Hybrid Systems [My Copy] Automated Reasoning with Analytic Tableaux and Related Methods (2007), pp. 216-232. by André Platzer posted to theorem-proving hybrid-systems dynamic-logic by robertjohnsimmons on 2009-10-17 21:15:02 as
	A proof-centric approach to mathematical assistants [My Copy] Journal of Applied Logic, Vol. 4, No. 4. (December 2006), pp. 505-532. by L. Dixon, J. Fleuriot posted to theorem-proving proof-assistants isabelle by robertjohnsimmons on 2009-10-11 18:49:18 as
	Mechanized Metatheory for the Masses: The PoplMark Challenge [My Copy] Theorem Proving in Higher Order Logics (2005), pp. 50-65. by Brian E. Aydemir, Aaron Bohannon, Matthew Fairbairn, et al.J. Nathan Foster, Benjamin C. Pierce, Peter Sewell, Dimitrios Vytiniotis, Geoffrey Washburn, Stephanie Weirich, Steve Zdancewic posted to twelf theorem-proving metatheory logical-frameworks isabelle evaluation-contexts coq by robertjohnsimmons on 2009-10-10 21:17:21 as
	Formal verification of a realistic compiler [My Copy] Commun. ACM, Vol. 52, No. 7. (2009), pp. 107-115. by Xavier Leroy posted to verification theorem-proving rg-2009 coq compilers by robertjohnsimmons to the group ConcertRG on 2009-10-10 00:45:31 as
	Functional programming and theorem proving for undergraduates: a progress report [My Copy] In FDPE '08: Proceedings of the 2008 international workshop on Functional and declarative programming in education (2008), pp. 21-30. by Rex Page, Carl Eastlund, Matthias Felleisen posted to theorem-proving pedagogy functional-programming acl2 by robertjohnsimmons on 2009-09-24 20:52:00 as
	Dependent types ensure partial correctness of theorem provers [My Copy] J. Funct. Program., Vol. 14, No. 1. (2004), pp. 3-19. by Andrew W. Appel, Amy P. Felty posted to dependent-types theorem-proving twelf by robertjohnsimmons on 2009-07-22 23:55:20 as
	Proving Theorems about LISP Functions [My Copy] Journal of the ACM, Vol. 22, No. 1. (January 1975), pp. 129-144. by Robert S. Boyer, J. Strother Moore posted to theorem-proving verification by mattmight on 2009-07-15 18:04:49 as along with 1 person radico
	Introduction To The Hol System [My Copy] HOL Theorem Proving System and Its Applications, 1991., International Workshop on the In HOL Theorem Proving System and Its Applications, 1991., International Workshop on the (1991), pp. 2-3. by Mike Gordon posted to theorem-proving verification by mattmight on 2009-07-15 18:01:50 as along with 1 person varming
	Coq in a Hurry [My Copy] (7 Nov 2008) by Yves Bertot posted to coq theorem-proving by mattmight on 2009-07-15 18:00:06 as along with 3 people shimomura _Anne_ jleny
	Completely non-clausal theorem proving [My Copy] Artificial Intelligence, Vol. 18, No. 1. (January 1982), pp. 67-85. by N. Murray posted to nonclausal-resolution resolution theorem-proving by robertjohnsimmons on 2009-07-07 13:06:53 as
	A machine program for theorem-proving [My Copy] Commun. ACM, Vol. 5, No. 7. (July 1962), pp. 394-397. by Martin Davis, George Logemann, Donald Loveland posted to algorithm boolean-satisfiability theorem-proving by brothers on 2009-07-07 05:02:15 as along with 6 people chsticksel gagliol bsilverthorn bulwahn bfraser voronov
	Taking Our Own Medicine: Applying the Refinement Calculus to State-Rich Refinement Model Checking [My Copy] Formal Methods and Software Engineering In Formal Methods and Software Engineering, Vol. 4260 (2006), pp. 697-716. by Leo Freitas, Ana Cavalcanti, Jim Woodcock posted to 2006 circus model-checking refinement-calculus theorem-proving verification by michaelbanks on 2009-07-02 12:02:13 as along with 1 person leonardo
	State-rich model checking [My Copy] Innovations in Systems and Software Engineering, Vol. 2, No. 1. (13 March 2006), pp. 49-64. by Leo Freitas, Jim Woodcock, Ana Cavalcanti posted to 2006 abstract-interpretation formal-methods model-checking theorem-proving tool verification by michaelbanks on 2009-07-02 11:34:50 as along with 1 person leonardo
	A direct path to dependable software [My Copy] Communications of the ACM, Vol. 52, No. 4. (2009), pp. 78-88. by Daniel Jackson posted to 2009 formal-methods model-checking testing theorem-proving by michaelbanks on 2009-06-24 14:13:40 as along with 2 people leonardo architect
	A Brief Overview of PVS [My Copy] Theorem Proving in Higher Order Logics In Theorem Proving in Higher Order Logics, Vol. 5170 (2008), pp. 22-27. by Sam Owre, Natarajan Shankar posted to 2008 pvs theorem-proving verification by michaelbanks on 2009-06-23 20:30:37 as along with 2 people mishra_satish leonardo
	On Automated Theorem Proving [My Copy] Annals of the New York Academy of Sciences In Frontiers of Science Reports from the Final International Session of the Moscow Refusnik Seminar, Vol. 661, No. 0. (1992), pp. 160-173. by Stephen Russell, Traci Wheeler posted to 2006 automatic theorem-proving by michaelbanks on 2009-05-20 19:03:05 as
	Theorem Proving for Verification (Invited Tutorial) [My Copy] Computer Aided Verification In Computer Aided Verification, Vol. 5123 (2008), pp. 11-18. by John Harrison posted to 2008 theorem-proving tutorial verification by michaelbanks on 2009-05-20 18:18:14 as along with 1 person dwei98
	Social Processes and Proofs of Theorems and Programs [My Copy] Communications of the ACM, Vol. 22, No. 5. (May 1979), pp. 271-280. by Richard A. Demillo, Richard J. Lipton, Alan J. Perlis posted to 1979 criticism formal-methods program social-processes theorem-proving verification by michaelbanks on 2009-05-18 11:27:32 as along with 2 people ljcamargos imrchen
	Verifying haskell programs using constructive type theory [My Copy] In Haskell '05: Proceedings of the 2005 ACM SIGPLAN workshop on Haskell (2005), pp. 62-73. by Andreas Abel, Marcin Benke, Ana Bove, John Hughes, Ulf Norell posted to agda dependent-types functional-programming haskell theorem-proving by jimburton on 2009-05-11 13:24:30 as along with 6 people and 1 group shimomura greenrd voigt p1738j msakai meiersi SRG_at_UCD
	Theorem Proving for Verification [My Copy] Modeling and Verification of Parallel Processes In Modeling and Verification of Parallel Processes, Vol. 2067 (2001), pp. 39-57. by John Rushby posted to 2001 concurrency model-checking safety theorem-proving verification by michaelbanks on 2009-05-05 16:59:13 as along with 2 people dwei98 mishra_satish
	Proof and System-Reliability (NATO Science Series II: Mathematics, Physics and Chemistry) [My Copy] (31 May 2002) posted to theorem-proving verification-tools by prahlad on 2009-05-03 12:48:36 as
	Proof Pearl: Mechanizing the Textbook Proof of Huffman’s Algorithm [My Copy] Journal of Automated Reasoning by Jasmin C. Blanchette posted to 2009 algorithm hol huffman isabelle mechanised proof theorem-proving by michaelbanks on 2009-03-12 10:13:38 as along with 1 person bulwahn
	Using the TPTP Language for Writing Derivations and Finite Interpretations [My Copy] Automated Reasoning (2006), pp. 67-81. by Geoff Sutcliffe, Stephan Schulz, Koen Claessen, Allen Van Gelder posted to theorem-proving by msakai on 2009-02-15 01:41:56 as
	Rewrite-based Equational Theorem Proving with Selection and Simplification [My Copy] J Logic Computation, Vol. 4, No. 3. (1 June 1994), pp. 217-247. by L. E. O. Bachmair, Harald Ganzinger posted to theorem-proving by msakai on 2009-01-29 15:20:49 as
	Automated Reasoning With Otter [My Copy] (10 January 2001) by John A. Kalman posted to theorem-proving by msakai on 2009-01-07 23:01:16 as
	Verifying the SET registration protocols [My Copy] IEEE J. of Selected Areas in Communications, Vol. 21 (2003) by Giampaolo Bella, Fabio, Lawrence C. Paulson posted to copy formal-method security theorem-proving by yoriyuki on 2009-01-07 02:57:31 as
	A verified model checker for the modal -calculus in Coq [My Copy] In In TACAS, volume 1384 of LNCS (1998) by Christoph Sprenger posted to agdaspin model-checking theorem-proving by yoriyuki on 2009-01-07 01:38:23 as
	1 Implementing a Model Checker for LEGO [My Copy] by Shenwei Yu, Zhaohui Luo posted to agdaspin copy model-checking print theorem-proving by yoriyuki on 2008-12-22 02:35:47 as
	What is the best way to prove a cryptographic protocol correct? [My Copy] IEEE International Symposium on Parallel and Distributed Processing (IPDPS 2008) In IEEE International Symposium on Parallel and Distributed Processing (IPDPS 2008) (2008), pp. 1-7. by Sreekanth Malladi, Gurdeep S. Hura posted to 2008 constraint-solving invariant protocol security theorem-proving verification by michaelbanks on 2008-12-02 13:13:15 as
	Z/Eves and the Mondex Electronic Purse [My Copy] Theoretical Aspects of Computing - ICTAC 2006 In Theoretical Aspects of Computing -- ICTAC 2006, Vol. 4281 (2006), pp. 15-34. by Jim Woodcock, Leo Freitas posted to 2006 grand-challenge mondex refinement security specification theorem-proving verification z z-eves by michaelbanks on 2008-11-02 15:25:46 as
	Routing Information Protocol in HOL/SPIN [My Copy] In TPHOLs '00: Proceedings of the 13th International Conference on Theorem Proving in Higher Order Logics (2000), pp. 53-72. by Karthikeyan Bhargavan, Carl A. Gunter, Davor Obradovic posted to agdaspin copy model-checking print spin theorem-proving by yoriyuki on 2008-10-07 06:26:29 as
	From LCF to HOL: a short history [My Copy] (2000), pp. 169-185. by Mike Gordon posted to domain-theory theorem-proving by msakai on 2008-10-07 01:09:43 as
	KAT-ML: An interactive theorem prover for Kleene Algebra with Tests [My Copy] Journal of Applied Non-Classical Logics, Vol. 16 (2003) by Kamal Aboul-Hosn, Dexter Kozen posted to kleene-algebra theorem-proving by msakai on 2008-10-05 16:37:36 as
	Automating Proofs in Category Theory [My Copy] Automated Reasoning (2006), pp. 392-407. by Dexter Kozen, Christoph Kreitz, Eva Richter posted to category-theory nuprl theorem-proving by spl on 2008-09-11 23:15:49 as along with 1 person prahlad
	Towards a Readable Formalisation of Category Theory [My Copy] Electronic Notes in Theoretical Computer Science In Proceedings of Computing: The Australasian Theory Symposium (CATS) 2004, Vol. 91 (16 February 2004), pp. 212-228. by Greg O'Keefe posted to category-theory formalization hol isabelle isar theorem-proving by spl on 2008-09-11 22:53:36 as along with 2 people prahlad maggesi
	Compositional Reasoning in Model Checking [My Copy] Lecture Notes in Computer Science, Vol. 1536 (1998), pp. 81-102. by Sergey Berezin, Sérgio Campos, Edmund M. Clarke posted to copy model-checking theorem-proving by yoriyuki on 2008-07-17 04:01:21 as along with 1 person msakai
	Verifying the SET registration protocols [My Copy] Selected Areas in Communications, IEEE Journal on In Selected Areas in Communications, IEEE Journal on, Vol. 21, No. 1. (2003), pp. 77-87. by G. Bella, F. Massacci, L. C. Paulson posted to copy formal-method network security theorem-proving by yoriyuki on 2008-07-01 03:20:41 as
	Guarded induction on final coalgebras [My Copy] Electronic Notes in Theoretical Computer Science (January 2004), pp. 1-18. by D. Pavlovic posted to category-theory coalgebra theorem-proving by msakai on 2008-06-01 05:09:27 as along with 1 person christiankissig
	Verifying CPS transformations in Isabelle/HOL [My Copy] In MERLIN '03: Proceedings of the 2003 workshop on Mechanized reasoning about languages with variable binding (2003), pp. 1-8. by Yasuhiko Minamide, Koji Okuma posted to continuation theorem-proving by msakai on 2008-05-28 12:27:00 as along with 2 people and 1 group dalev mvermaat NU-PRL
	Verifying Haskell programs by combining testing, model checking and interactive theorem proving [My Copy] Information and Software Technology In Third International Conference on Quality Software: QSIC 2003, Vol. 46, No. 15. (1 December 2004), pp. 1011-1025. by Peter Dybjer, Qiao Haiyan, Makoto Takeyama posted to haskell model-checking theorem-proving by msakai on 2008-05-28 12:20:45 as along with 2 people pmatos shimomura
	Theorem proving support in programming language semantics [My Copy] (6 Jul 2007) by Yves Bertot posted to coq semantics theorem-proving by mvermaat on 2008-04-16 15:02:02 as along with 4 people _Anne_ jrw bunge robotact
	Subset Coercions in Coq [My Copy] Types for Proofs and Programs In Types for Proofs and Programs (2007), pp. 237-252. by Matthieu Sozeau edited by Thorsten Altenkirch, Conor Mcbride posted to coq dependent-types functional-programming theorem-proving type-theory by jimburton on 2008-02-28 13:56:18 as along with 1 person pedagand
	Mechanizing common knowledge logic using COQ [My Copy] Annals of Mathematics and Artificial Intelligence, Vol. 48, No. 1-2. (September 2006), pp. 15-43. by Lescanne, Pierre posted to theorem-proving by msakai on 2007-12-16 04:39:18 as
	An interpolating theorem prover [My Copy] Theoretical Computer Science, Vol. 345, No. 1. (21 November 2005), pp. 101-121. by K. McMillan posted to model-checking theorem-proving by msakai on 2007-11-11 10:38:04 as along with 1 person rhishi
	Mechanically Proving Geometry Theorems Using a Combination of Wu's Method and Collins' Method [My Copy] In CADE-12: Proceedings of the 12th International Conference on Automated Deduction (1994), pp. 401-415. by Nicholas F. Mcphee, Shang-Ching Chou, Xiao-Shan Gao posted to automated-reasoning geometry theorem-proving by mcphee on 2007-09-10 11:20:59 as
	A New Approach for Automatic Theorem Proving in Real Geometry [My Copy] Journal of Automated Reasoning, Vol. 21, No. 3. (1998), pp. 357-380. by Andreas Dolzmann, Thomas Sturm, Volker Weispfenning posted to automated-reasoning geometry theorem-proving by mcphee on 2007-09-10 11:10:22 as
	New results on rewrite-based satisfiability procedures [My Copy] (22 Nov 2006) by Alessandro Armando, Maria P. Bonacina, Silvio Ranise, Stephan Schulz posted to acquaintances theorem-proving by dmitri83 on 2006-12-10 02:29:19 as
	Formalising Sylow's theorems in Coq [My Copy] (14 Nov 2006) by Laurent Thery posted to theorem-proving by dmitri83 on 2006-11-25 21:32:55 as along with 1 person proportional

Note: You may cite this page as: http://www.citeulike.org/tag/theorem-proving

Result page: 1 2 Next

verification	20
model-checking	10
coq	7
dependent-types	7
isabelle	6
acl2	5
copy	5
2006	4
alpha-equivalence	4
functional-programming	4
security	4
2008	3
2009	3
agdaspin	3
category-theory	3
formal-methods	3
semantics	3
algorithm	2
athena	2
automated-reasoning	2
calculemus	2
compilers	2
cps	2
curry-howard	2
dpl	2
epigram	2
formal-method	2
formal-modeling	2
geometry	2
haskell	2
hol	2
lisp	2
print	2
proof	2
proof-language	2
symbolic-computation	2
symbolic-execution	2
twelf	2
type-checking	2
verification-tools	2
z	2
1979	1
2001	1
abstract-interpretation	1
acquaintances	1
agda	1
alloy	1
automatic	1
boolean-satisfiability	1
circus	1
coalgebra	1
coinduction	1
concurrency	1
constraint-solving	1
continuation	1
criticism	1
domain-theory	1
dynamic-logic	1
evaluation-contexts	1
formalization	1
grand-challenge	1
hardcopy	1
huffman	1
hybrid-systems	1
invariant	1
isar	1
kleene-algebra	1
lics01	1
logic	1
logical-frameworks	1
master-project	1
mechanised	1
metatheory	1
mondex	1
network	1
nonclausal-resolution	1
nuprl	1
pedagogy	1
program	1
program-analysis	1
programming-languages	1
proof-assistants	1
protocol	1
pvs	1
reasoning	1
recursion	1
refinement	1
refinement-calculus	1
resolution	1
rg-2009	1
safety	1
social-processes	1
specification	1
spin	1
testing	1
tool	1
tutorial	1
type-theory	1
utp	1
z-eves	1

Tag theorem-proving [59 articles] Export

Related Tags