TPHOLS 2004 : theorem proving in higher order logics (Park City UT, 14-17 September 2004)Slind, Konrad; Bunker, Annette; Gopalakrishnan, Ganesh et al.Lecture notes in computer science. 2004, issn 0302-9743, isbn 3-540-23017-3, VIII, 336 p, isbn 3-540-23017-3Conference Proceedings

TPHOLs 2001 : theorem proving in higher order logics (Edinburgh, 3-6 September 2001)Boulton, Richard J; Jackson, Paul B.Lecture notes in computer science. 2001, issn 0302-9743, isbn 3-540-42525-X, X, 393 p, isbn 3-540-42525-XConference Proceedings

Mizar light for HOL lightWIEDIJK, Freek.Lecture notes in computer science. 2001, pp 378-393, issn 0302-9743, isbn 3-540-42525-XConference Paper

An improved extensionality criterion for higher-order logic programsBEZEM, Marc.Lecture notes in computer science. 2001, pp 203-216, issn 0302-9743, isbn 3-540-42554-3Conference Paper

Nuprl-Light : An implementation framework for higher-order logicsHICKEY, J. J.Lecture notes in computer science. 1997, pp 395-399, issn 0302-9743, isbn 3-540-63104-6Conference Paper

Predicate subtyping with predicate setsHURD, Joe.Lecture notes in computer science. 2001, pp 265-280, issn 0302-9743, isbn 3-540-42525-XConference Paper

Higher-order transformation of logic programsSERES, Silvija; SPIVEY, Michael.Lecture notes in computer science. 2001, Vol 2042, pp 57-68, issn 0302-9743, isbn 3-540-42127-0Conference Paper

A new logical characterization of Büchi automataLENZI, Giacomo.Lecture notes in computer science. 2001, pp 467-477, issn 0302-9743, isbn 3-540-41695-1Conference Paper

Combining Higher Order Abstract Syntax with tactical theorem proving and (co)inductionAMBLER, Simon J; CROLE, Roy L; MOMIGLIANO, Alberto et al.Lecture notes in computer science. 2002, pp 13-30, issn 0302-9743, isbn 3-540-44039-9, 18 p.Conference Paper

Calculational reasoning revisited : An Isabelle/Isar experienceBAUER, Gertrud; WENZEL, Markus.Lecture notes in computer science. 2001, pp 75-90, issn 0302-9743, isbn 3-540-42525-XConference Paper

Idempotent Relations in Isabelle/HOLKAMMÜLLER, Florian; SANDERS, J. W.Lecture notes in computer science. 2005, pp 310-324, issn 0302-9743, isbn 3-540-25304-1, 15 p.Conference Paper

Reasoning about CBV functional programs in Isabelle/HOLLONGLEY, John; POLLACK, Randy.Lecture notes in computer science. 2004, pp 201-216, issn 0302-9743, isbn 3-540-23017-3, 16 p.Conference Paper

A type-theoretic memory model for verification of sequential Java programsVAN DEN BERG, Joachim; HUISMAN, Marieke; JACOBS, Bart et al.Lecture notes in computer science. 2000, pp 1-21, issn 0302-9743, isbn 3-540-67898-0Conference Paper

Axiomatising tree-interpretable structuresBLUMENSATH, Achim.Lecture notes in computer science. 2002, pp 596-607, issn 0302-9743, isbn 3-540-43283-3Conference Paper

MONA implementation secretsKLARLUND, Nils; MØLLER, Anders; SCHWARTZBACH, Michael I et al.Lecture notes in computer science. 2001, pp 182-194, issn 0302-9743, isbn 3-540-42491-1Conference Paper

0-1 Laws for fragments of existential second-order logic : A surveyKOLAITIS, P. G; VARDI, M. Y.Lecture notes in computer science. 2000, pp 84-98, issn 0302-9743, isbn 3-540-67901-4Conference Paper

Higher-order logic and theorem proving for structured specificationsBORZYSZKOWSKI, Tomasz.Lecture notes in computer science. 2000, pp 401-418, issn 0302-9743, isbn 3-540-67898-0Conference Paper

WADT'99 : recent trends in algebraic development techniques (Château de Bonas, 15-18 September 1999)Bert, Didier; Choppy, Christine; Mosses, Peter et al.Lecture notes in computer science. 2000, issn 0302-9743, isbn 3-540-67898-0, X, 476 p, isbn 3-540-67898-0Conference Proceedings

A new model construction for the polymorphic lambda calculusSPREEN, Dieter.Lecture notes in computer science. 2000, pp 275-292, issn 0302-9743, isbn 3-540-41285-9Conference Paper

(Agnostic) PAC learning concepts in higher-order logicNG, K. S.Lecture notes in computer science. 2006, pp 711-718, issn 0302-9743, isbn 3-540-45375-X, 1Vol, 8 p.Conference Paper

Learning comprehensible theories from structured dataLLOYD, J. W.Lecture notes in computer science. 2003, pp 203-225, issn 0302-9743, isbn 3-540-00529-3, 23 p.Conference Paper

Proof pearl : Using combinators to manipulate let-expressions in proofNORRISH, Michael; SLIND, Konrad.Lecture notes in computer science. 2005, pp 397-408, issn 0302-9743, isbn 3-540-28372-2, 12 p.Conference Paper

Holes with binding powerJOJGOV, Georgi I.Lecture notes in computer science. 2003, pp 162-181, issn 0302-9743, isbn 3-540-14031-X, 20 p.Conference Paper

TPHOLs 2002 : theorem proving in higher order logics (Hampton VA, 20-23 August 2002)Carrano, Victor; Munoz, César A; Tahar, Sofiène et al.Lecture notes in computer science. 2002, issn 0302-9743, isbn 3-540-44039-9, X, 347 p, isbn 3-540-44039-9Conference Proceedings

The complexity of translating logic to finite automataREINHARDT, Klaus.Lecture notes in computer science. 2002, pp 231-238, issn 0302-9743, isbn 3-540-00388-6, 8 p.Conference Paper