A Modal Lambda Calculus with Iteration and Case Constructs | Zendy

Joëlle Despeyroux | Zendy; Pierre Leleu | Zendy

AI Assistant Blog Pricing

Home ZAIA Blog

Open Access

A Modal Lambda Calculus with Iteration and Case Constructs

Author(s) -

Joëlle Despeyroux,

Pierre Leleu

Publication year - 1999

Publication title -

lecture notes in computer science

Language(s) - English

Resource type - Book series

SCImago Journal Rank - 0.249

H-Index - 400

eISSN - 1611-3349

pISSN - 0302-9743

ISBN - 3-540-66537-4

DOI - 10.1007/3-540-48167-2_4

Subject(s) - soundness , calculus (dental) , modal , mathematics , modal logic , decidability , modal operator , simply typed lambda calculus , algebra over a field , natural deduction , lambda calculus , reduction (mathematics) , modal μ calculus , normalization (sociology) , bisimulation , computer science , discrete mathematics , typed lambda calculus , pure mathematics , normal modal logic , programming language , medicine , chemistry , geometry , dentistry , sociology , anthropology , polymer chemistry

An extension of the simply-typed -calculus, allowing iteration and case reasoning over terms of functional types that arise when using higher order abstract syntax, has recently been introduced by Joëlle Despeyroux, Frank Pfenning and Carsten Sch¨1rmann. This thorny mixing is achieved thanks to the help of the operator ` " of modal logic S4. Here we give a new presentation of their system, with reduction rules, instead of evaluation judgments, that compute the canonical forms of terms. Our...

The content you want is available to Zendy users.

Already have an account? Click here to sign in.

Having issues? You can contact us here

Accelerating Research