Higher Order Logic Theorem Proving and Its Applications: 6th International Workshop, HUG '93, Vancouver, B.C., Canada, August 11-13, 1993 : ProceedingsSpringer-Verlag, 1994 - 517 من الصفحات This volume constitutes the refereed proceedings of the 1993 Higher-Order Logic User's Group Workshop, held at the University of British Columbia in August 1993. The workshop was sponsored by the Centre for Integrated Computer System Research. It was the sixth in the series of annual international workshops dedicated to the topic of Higher-Order Logic theorem proving, its usage in the HOL system, and its applications. The volume contains 40 papers, including an invited paper by David Parnas, McMaster University, Canada, entitled "Some theorems we should prove." |
المحتوى
Program Verification using HOLUNITY F Andersen K D Petersen | 1 |
Graph model of LAMBDA in Higher Order Logic K D Petersen Tele | 16 |
Mechanizing a Programming Logic for the Concurrent Programming Lan | 29 |
حقوق النشر | |
28 من الأقسام الأخرى غير ظاهرة
طبعات أخرى - عرض جميع المقتطفات
عبارات ومصطلحات مألوفة
abstraction algorithm applied approach assertions automated automatically behaviour bool boolean buffered circuits Computer Science construction constructors corresponding defined definition denotes derived described domain embedding equations evaluation example expressions finite formal formal verification formulae FSM-goals function given goal hardware description languages hardware verification Higher Order Logic higher-order logic Hoare logic HOL theorem prover implementation induction inference rules input instantiation instruction interpreter invocval pname label LAMBDA lemma lift Melham microprocessor microSR natural numbers Nuprl operation operational semantics output paper predicate proof system properties prove pure CCS PWORDLEN quantified recursive type relation represented reset result rewriting satisfies semantics signals Silage simulation specification Standard ML step structural subgoals subset subtrees symbolic syntax tactic Technical Report temporal theorem prover theory tion transition translation University University of Cambridge value-passing variables Viper