Max-Planck-Institut für Informatik
max planck institut
informatik
mpii logo Minerva of the Max Planck Society
 

Publications Master Template :: Thesis :: Ayari, Abdelwaheb


Publications Master Template
Show all entries of:this year (2019)last year (2018)two years ago (2017)Open in Notes
Action:login to update

Thesis - Master's thesis | @MastersThesis | Masterarbeit


Author
Author(s)*:Ayari, Abdelwaheb
BibTeX citekey*:Abdu95
Language:English

Title, School
Title*:A Reinterpretation of the Deductive Tableaux System in Higher-Order Logic
School:Universität des Saarlandes
Type of Thesis*:Master's thesis
Month:June
Year:1995


Note, Abstract, Copyright
LaTeX Abstract:Our research investigates frameworks supporting the formalization of programming calculi and their application to deduction-based progr am synthesis. Here we report on a case study: within a conservative extension of higher-order logic implemented in the Isabelle system, we derived rules for program development which can simulate those of the deductive tableau proposed by Manna and Waldinger. We have used the resulting theory to synthesize a library of verified programs, focusing in particular on sorting algorithms. Our experience suggests that the methodology we propose is well suited both to implement and use programming calculi, extend them, partially automate them, and even formally reason about their correctness.
Download Access Level:Public
Download File(s):View attachments here:

Referees, Status, Dates
1. Referee:Harald Ganzinger
2. Referee:David Basin
Supervisor:David Basin
Status:Completed
Date Kolloquium:18 August 2019

Correlation
MPG Unit:Max-Planck-Institut für Informatik
MPG Subunit:Programming Logics Group
Audience:Expert
Appearance:MPII WWW Server, MPII FTP Server, MPG publications list

BibTeX Entry:

@MASTERSTHESIS{Abdu95,
AUTHOR = {Ayari, Abdelwaheb},
TITLE = {A Reinterpretation of the Deductive Tableaux System in Higher-Order Logic},
SCHOOL = {Universit{\"a}t des Saarlandes},
YEAR = {1995},
TYPE = {Master's thesis}
MONTH = {June},
}


Hide details for Attachment SectionAttachment Section

View attachments here:




Entry last modified by Uwe Brahm, 03/12/2010
Hide details for Edit History (please click the blue arrow to see the details)Edit History (please click the blue arrow to see the details)

Editor(s)
Uwe Brahm
Created
03/25/1996 06:07:47 PM
Revisions
6.
5.
4.
3.
2.
Editor(s)
Uwe Brahm
Uwe Brahm
Uwe Brahm
Christine Kiesel
Christine Kiesel
Edit Dates
07/11/2007 10:15:21
03/23/98 06:56:53 PM
28.11.96 17:37:45
28/11/96 14:54:25
10/07/96 22:32:34