Higher Order Proof Systems
{'Code': '05010400', 'Directorate': {'LongName': 'Direct For Computer & Info Scie & Enginr'}, 'Division': {'LongName': 'Division of Computing and Communication Foundations'}}
{'SignBlockName': 'S. Kamal Abdali'}
This project will investigate the nature of computational systems which         are meant to discover proofs and compute with them after they are               discovered.  The concept of proofs-as-values is not only interesting in         its own right but also central for the development of interesting               theorem provers and proof assistants for use by mathematicians and              computer scientists.  As a guide in designing such proof systems,               several relevant issues in the semantics of constructive logics and             higher-order polymorphic  \-calculus will be investigated.  A clear             understanding of such models would help in developing a consistent and          clean programming paradigm for the implementation of higher-order proof         systems.  The project will also investigate the role which extensions           of logic programming languages could play as the underlying                     implementation languages for higher-order proof systems.  The central           role of search and equation solving (unification) in logic programming          may make it more suitable for the implementation of proof systems than          more traditionally used languages such as ML.
[{'FirstName': 'Andre', 'LastName': 'Scedrov', 'EmailAddress': 'scedrov@math.upenn.edu', 'StartDate': '08/15/1987', 'EndDate': None, 'RoleCode': 'Co-Principal Investigator'}, {'FirstName': 'Dale', 'LastName': 'Miller', 'EmailAddress': 'dale@cse.psu.edu', 'StartDate': '08/15/1987', 'EndDate': None, 'RoleCode': 'Principal Investigator'}]
{'Name': 'University of Pennsylvania', 'CityName': 'Philadelphia', 'ZipCode': '191046205', 'PhoneNumber': '2158987293', 'StreetAddress': 'Research Services', 'CountryName': 'United States', 'StateName': 'Pennsylvania', 'StateCode': 'PA'}
[{'Code': '2865', 'Text': 'NUMERIC, SYMBOLIC & GEO COMPUT'}, {'Code': '2875', 'Text': 'SYSTEM SOFTWARE'}]
{'url': 'https://www.nsf.gov/awardsearch/download?DownloadFileName=1987&All=true', 'xml': '8705596.xml'}