เทอมเคอร์รี-โฮวาร์ดเป็นเทอมแลมบ์ดาชนิดไทป์ซึ่งสามารถใช้เป็นตัวแทนบทพิสูจน์รูปนัยในระบบนิรนัยธรรมชาติ และการสร้างเทอมเคอร์รี-โฮวาร์ดนี้เป็นวิธีการมาตรฐานในการสร้างโปรแกรมจากบทพิสูจน์ ในการพิสูจน์ทางคณิตศาสตร์ แบบรูปที่เหมือนกันมักเกิดขึ้นบ่อยครั้ง ดังนั้นในการสร้างโปรแกรมจากบทพิสูจน์จะเป็นประโยชน์ถ้ามีการนิยามแบบรูปหรือเทมเพลตอย่างเป็นแบบแผนแล้วเติมเข้าไปในระบบ เพื่อที่เราจะได้ไม่ต้องทำสิ่งที่เหมือน ๆ กันซ้ำแล้วซ้ำอีก ยิ่งกว่านั้นการทำเช่นนี้ยังสะท้อนสิ่งที่ปฏิบัติกันตามปรกติในคณิตศาสตร์ ในงานวิจัยนี้เราสร้างระบบใหม่สำหรับการสร้างโปรแกรมจากบทพิสูจน์ ด้วยการขยายระบบของครอสสลีย์และเชเพอร์ดสันซึ่งสร้างในภาษาของแคลคูลัสภาคแสดงอันดับที่หนึ่ง(ใน[3]) ไปสู่ตรรกศาสตร์อันดับที่สองและเติมเทมเพลตในฐานะกฎใหม่เข้าไปในระบบที่ขยายนี้ เราสร้างเทมเพลตสองชนิดคือเทมเพลตแบบอุปนัยและเทมเพลตแบบการย่อ เทมเพลตแบบแรกทำให้เราสามารถใช้อุปนัยแบบต่าง ๆ ในระบบรูปนัยโดยไม่ต้องผ่านจำนวนธรรมชาติและเทมเพลตแบบหลังทำให้เราสามารถย่อประโยคทางคณิตศาสตร์ในบทพิสูจน์รูปนัยด้วยเพรดิเคตใหม่ เทอมเคอร์รี-โฮวาร์ดที่สร้างขึ้นในระบบใหม่นี้ยังคงมีสมบัติพื้นฐานรวมทั้งยังสอดคล้องกับทฤษฎีนอร์มาไลเซชันแบบเข้ม เราจึงสามารถขยายการสร้างโปรแกรมไปสู่ระบบตรรกศาสตร์ที่กว้างกว่ามาก