Realisability Interpretation and Rule Schemata

Add to your list(s) Download to your calendar using vCal

• Caroline Hou, Dept. of Computer Science, University of Swansea
• Friday 13 June 2014, 12:00-12:30
• Mahanakorn Lab, EEE.

If you have a question about this talk, please contact Wiesia R Hsissen.

The methodologies for designing reliable software can be viewed as either based on correctness proofs (i.e., giving proofs for existing programs) or on program extractions (i.e., from proofs to generate programs). The correctness of an extracted program is guaranteed by construction. One method of program extraction is to employ a realisability interpretation.

I will start by giving a realisability interpretation of an intuitionistic version of Church’s Simple Theory of Types which can be viewed as a formalisation of intuitionistic higher-order logic. Subsequently, I will introduce a uniform system of rule schemata to generate proof rules for different styles of logical calculi. The system is inspired by the coding of a prototype interactive theorem prover whose intention is to demonstrate the usefulness of the theory described above.

This talk is part of the Circuits and Systems Group: Internal Seminars series.

This talk is included in these lists:

• Andrea Picciau's list
• COMMSP & CP list
• COMMSP Seminar
• Circuits and Systems Group: Internal Seminars
• Featured talks
• Mahanakorn Lab, EEE
• SAP Talks

Note that ex-directory lists are not shown.