Home › Digital Repository › Faculty, Staff and Student Publications/Presentations › Undergraduate Research › Undergraduate Research Day › Undergraduate Research Day 2010 ›

Scheme Theorem Proving For Pedagogical Purposes With ...

Object Details

View

Title Information
Scheme Theorem Proving For Pedagogical Purposes With ACL2

Name:Personal
Christopher MacLellan Role :Text(marcrelator)
creator

Name:Personal
Melissa Wiederrecht Role :Text(marcrelator)
creator

Name:Personal
Professor Ruben Gamboa Role :Text(marcrelator)
creator

typeOfResource
text genre
Powerpoint/PDF
Origin Information Place
Laramie, Wyoming
University of Wyoming (keyDate="yes")
4/24/2010

Physical Description
born digital

abstract
Beginning programming students could benefit very much from having more feedback about their programs as the work than the standard syntax checking. It would be very useful if they could have an immediate proof of logical correctness or feedback as to where their logic is faulty. As a first step toward the ultimate goal of having this built in Scheme, we built an interpreter for the Dr. Scheme Beginning Student Language in ACL2 and proved many theorems in ACL2 about the correctness of programs written in our interpreter. This helps us to see some of the ways of thinking about Scheme proofs that can greatly assist when it comes to building the prover in Scheme. note
From - Undergraduate Research Day 2010 - Celebration of Research - Abstracts
Subject
Undergraduate Research Day

Related Item:Host Title Information
Undergraduate Research Day 2010

Location (usage="primary display")
http://hdl.handle.net/10176/wyu:751

accessCondition:useAndReproduction
http://digital.uwyo.edu/copyright.htm