On this page:
Invited Speakers
- Jean-Yves Girard:
Quantitative and Qualitative SemanticsMore Information... - Anil Nerode:
A Logician Looks at Expert Systems: Areas for Mathematical ResearchMore Information... - John Alan Robinson:
Merging Functional with Relational Programming in a Reduction SettingMore Information...
Presented Papers
Entries are ordered by surname of first author
- Martín Abadi Zohar Manna:
A Timely ResolutionMore Information... - Roberto M. Amadio Kim B. Bruce Giuseppe Longo:
The Finitary Projection Model for Second Order Lambda Calculus and Solutions to Higher Order Domain EquationsMore Information... - Leo Bachmair Nachum Dershowitz Jieh Hsiang:
Orderings for Equational ProofsMore Information... - Lennart Beckman Rune Gustavsson Annika Wærn:
An Algebraic Model of Parallel Execution of Logic ProgramsMore Information... - David B. Benson Ofer Ben-Shachar:
Strong Bisimulation of State AutomataMore Information... - Stephen D. Brookes:
A Semantically Based Proof System for Partial Correctness and Deadlock in CSPMore Information... - Michael C. Browne:
An Improved Algorithm for the Automatic Verification of Finite State Systems Using Temporal LogicMore Information... - Shang-Ching Chou Hai-Ping Ko:
On Mechanical Theorem Proving in Minkowskian Plane GeometryMore Information... - Mario Coppo Maddalena Zacchi:
Type inference and logical relationsMore Information... - Thierry Coquand:
An Analysis of Girard's ParadoxMore Information... - László Csirmaz Bradd Hart:
Program Correctness on Finite FieldsMore Information... - Joëlle Despeyroux:
Proof of Translation in Natural SemanticsMore Information... - E. Allen Emerson Chin-Laung Lei:
Efficient Model Checking in Fragments of the Propositional Mu-Calculus (Extended Abstract)More Information... - Matthias Felleisen Daniel P. Friedman Eugene E. Kohlbecker Bruce F. Duba:
Reasoning with ContinuationsMore Information... - Steven M. German Edmund M. Clarke Joseph Y. Halpern:
True Relative Completeness of an Axiom System for the Language L4 (Abridged)More Information... - Carl A. Gunter:
The Largest First-Order-Axiomatizable Cartesian Closed Category of DomainsMore Information... - Joseph Y. Halpern John H. Williams Edward L. Wimmers:
Good Rewrite Strategies for FPMore Information... - Joseph Y. Halpern Yoav Shoham:
A Propositional Model Logic of Time IntervalsMore Information... - Bengt Jonsson Zohar Manna Richard J. Waldinger:
Towards Deductive Synthesis of Dataflow NetworksMore Information... - Jean-Pierre Jouannaud Emmanuel Kounalis:
Automatic Proofs by Induction in Equational Theories Without ConstructorsMore Information... - Deepak Kapur David R. Musser:
Inductive Reasoning with Incomplete Specifications (Preliminary Report)More Information... - Claude Kirchner:
Computing Unification AlgorithmsMore Information... - Todd B. Knoblock Robert L. Constable:
Formalized Metareasoning in Type TheoryMore Information... - Johann A. Makowsky Ildikó Sain:
On the Equivalence of Weak Second Order and Nonstandard Time Semantics For Various Program Verification SystemsMore Information... - Ian A. Mason:
Equivalence of First Order LISP Programs. Proving Properties of Destructive Programs via TransformationMore Information... - N. P. Mendler Prakash Panangaden Robert L. Constable:
Infinite Objects in Type TheoryMore Information... - Albert R. Meyer:
Floyd-Hoare Logic Defines Semantics: Preliminary VersionMore Information... - Christine Mohring:
Algorithm Development in the Calculus of ConstructionsMore Information... - Luís Monteiro Fernando C. N. Pereira:
A Sheaf-Theoretic Model of ConcurrencyMore Information... - Rohit Parikh:
Levels of Knowledge in Distributed ComputingMore Information... - Dominique Perrin Paul E. Schupp:
Automata on the Integers, Recurrence Distinguishability, and the Equivalence and Decidability of Monadic TheoriesMore Information... - David A. Plaisted:
The Denotional Semantics of Nondeterministic Recursive Programs using Coherent RelationsMore Information... - Amir Pnueli Lenore D. Zuck:
Probabilistic Verification by TableauxMore Information... - Roni Rosner Amir Pnueli:
A Choppy LogicMore Information... - William C. Rounds Robert T. Kasper:
A Complete Logical Calculus for Record Structures Representing Linguistic InformationMore Information... - John S. Schlipf:
How Uncomputable is General Circumscription? (Extended Abstract)More Information... - J. Shultis:
The Design and Implementations of IntuitMore Information... - Richard Statman:
On Translating Lambda Terms into Combinators; The Basis ProblemMore Information... - Moshe Y. Vardi Pierre Wolper:
An Automata-Theoretic Approach to Automatic Program Verification (Preliminary Report)More Information...
Organizers
Program ChairAlbert Meyer |
Program Committee:R. Boyer; W. Damm; S. German; D. Gries; M. Hennessy; G. Huet; D. Kozen; A. Meyer (chair); J. Mitchell; R. Parikh; G. Plotkin; J. Reynolds; J. Robinson; D. Scott; M. Vardi; R. Waldinger |