ترغب بنشر مسار تعليمي؟ اضغط هنا

Certified proofs in programs involving exceptions

186   0   0.0 ( 0 )
 نشر من قبل Jean-Guillaume Dumas
 تاريخ النشر 2013
  مجال البحث الهندسة المعلوماتية
والبحث باللغة English




اسأل ChatGPT حول البحث

Exception handling is provided by most modern programming languages. It allows to deal with anomalous or exceptional events which require special processing. In computer algebra, exception handling is an efficient way to implement the dynamic evaluation paradigm: for instance, in linear algebra, dynamic evaluation can be used for applying programs which have been written for matrices with coefficients in a field to matrices with coefficients in a ring. Thus, a proof system for computer algebra should include a treatement of exceptions, which must rely on a careful description of a semantics of exceptions. The categorical notion of monad can be used for formalizing the raising of exceptions: this has been proposed by Moggi and implemented in Haskell. In this paper, we provide a proof system for exceptions which involves both raising and handling, by extending Moggis approach. Moreover, the core part of this proof system is dual to a proof system for side effects in imperative languages, which relies on the categorical notion of comonad. Both proof systems are implemented in the Coq proof assistant.



قيم البحث

اقرأ أيضاً

We define a proof system for exceptions which is close to the syntax for exceptions, in the sense that the exceptions do not appear explicitly in the type of any expression. This proof system is sound with respect to the intended denotational semanti cs of exceptions. With this inference system we prove several properties of exceptions.
102 - Federico Aschieri 2018
We introduce a first proofs-as-parallel-programs correspondence for classical logic. We define a parallel and more powerful extension of the simply typed lambda calculus corresponding to an analytic natural deduction based on the excluded middle law. The resulting functional language features a natural higher-order communication mechanism between processes, which also supports broadcasting. The normalization procedure makes use of reductions that implement novel techniques for handling and transmitting process closures.
An algebraic method is used to study the semantics of exceptions in computer languages. The exceptions form a computational effect, in the sense that there is an apparent mismatch between the syntax of exceptions and their intended semantics. We solv e this apparent contradiction by efining a logic for exceptions with a proof system which is close to their syntax and where their intended semantics can be seen as a model. This requires a robust framework for logics and their morphisms, which is provided by categorical tools relying on adjunctions, fractions and limit sketches.
In this short note we study the semantics of two basic computational effects, exceptions and states, from a new point of view. In the handling of exceptions we dissociate the control from the elementary operation which recovers from the exception. In this way it becomes apparent that there is a duality, in the categorical sense, between exceptions and states.
In this article we present an ongoing effort to formalise quantum algorithms and results in quantum information theory using the proof assistant Isabelle/HOL. Formal methods being critical for the safety and security of algorithms and protocols, we f oresee their widespread use for quantum computing in the future. We have developed a large library for quantum computing in Isabelle based on a matrix representation for quantum circuits, successfully formalising the no-cloning theorem, quantum teleportation, Deutschs algorithm, the Deutsch-Jozsa algorithm and the quantum Prisoners Dilemma. We discuss the design choices made and report on an outcome of our work in the field of quantum game theory.
التعليقات
جاري جلب التعليقات جاري جلب التعليقات
سجل دخول لتتمكن من متابعة معايير البحث التي قمت باختيارها
mircosoft-partner

هل ترغب بارسال اشعارات عن اخر التحديثات في شمرا-اكاديميا