268:
is represented by its signature which assigns kinds and types to a finite set of constants that represents its syntax, its judgements and its rule schemes. An object-logic's rules and proofs are seen as primitive proofs of hypothetico-general judgements
317:
241:, correspond to the ordinary and dependent function space, respectively. The methodology of judgements-as-types is that judgements are represented as the types of their proofs. A
239:
441:
Language
Engineering and Rigorous Software Development: International LerNet ALFA Summer School 2008, Piriapolis, Uruguay, February 24 - March 1, 2008, Revised, Selected Papers
266:
724:
662:
628:
195:
572:
132:. The key features of the λΠ-calculus are that it consists of entities of three levels: objects, types and kinds (or type classes, or families of types). It is
773:
580:
494:
449:
422:
391:
63:
are based on this idea. Unlike a direct embedding, the logical framework approach allows many logics to be embedded in the same type system.
758:
503:
486:
122:
168:
584:
327:
768:
272:
60:
48:
595:
532:
200:
473:
354:
72:
763:
145:
137:
247:
706:
644:
610:
359:
47:
problem in the framework type theory. This approach has been used successfully for (interactive)
174:
557:
490:
445:
418:
408:
387:
160:
126:
118:
76:
71:
A logical framework is based on a general treatment of syntax, rules and proofs by means of a
55:; however, the name of the idea comes from the more widely known Edinburgh Logical Framework,
44:
40:
439:
414:
133:
666:. In: G. Huet and G. Plotkin (eds), Logical Frameworks, Cambridge University Press, 1991.
687:. In M. Bezem, J.F. Groote (Eds.), Typed Lambda Calculi and Applications. Volume 664 of
742:
636:
507:
469:
242:
149:
17:
752:
164:
141:
129:
599:
121:. This is a system of first-order dependent function types which are related by the
581:
On the
Meanings of the Logical Constants and the Justifications of the Logical Laws
35:
provides a means to define (or present) a logic as a signature in a higher-order
517:
477:
171:, in the 1983 Siena Lectures. The two higher-order judgements, the hypothetical
36:
680:. Technical Report, University of Edinburgh, 1992. LFCS report ECS-LFCS-92-227.
341:
728:
International
Journal of Foundations of Computer Science 3(3), 333-378, 1992.
738:
337:
meta-theoretic reasoning about logic programs (termination, coverage, etc.)
92:
A characterization of the mechanism by which object-logics are represented.
514:. Journal of the Association for Computing Machinery, 40(1):143-184, 1993.
159:
by the judgements-as-types representation mechanism. This is inspired by
52:
522:
Using typed lambda calculus to implement formal systems on a machine
86:
A characterization of the class of object-logics to be represented;
323:
28:
322:
An implementation of the LF logical framework is provided by the
82:
To describe a logical framework, one must provide the following:
75:. Syntax is treated in a style similar to, but more general than
253:
685:
The undecidability of typability in the lambda-pi-calculus
576:. Journal of Logic and Computation 12(6), 1061-1104, 2002.
542:. Annals of Pure and Applied Logic, 67(1-3):113-160, 1994.
540:
671:
Proof-search in type-theoretic languages:an introduction
472:(2002). "Logical frameworks – a brief introduction". In
554:
Kripke
Resource Models of a Dependently-typed, Bunched
709:
647:
613:
560:
538:
Robert Harper, Donald
Sannella and Andrzej Tarlecki.
438:
Ana Bove; Luis Soares
Barbosa; Alberto Pardo (2009).
275:
250:
203:
177:
590:
Bengt
Nordström, Kent Petersson, and Jan M. Smith.
549:. Journal of Logic and Computation 8, 809-838, 1998.
718:
656:
622:
566:
524:. Journal of Automated Reasoning, 9:309-354, 1992.
311:
260:
233:
189:
43:of a formula in the original logic reduces to a
739:Specific Logical Frameworks and Implementations
696:Proofs, Search and Computation in General Logic
673:. Theoretical Computer Science 232 (2000) 5-53.
698:. Ph.D. thesis, University of Edinburgh, 1990.
520:, Furio Honsell, Ian Mason and Randy Pollack.
8:
377:
375:
312:{\displaystyle \Lambda x\in C.J(x)\vdash K}
708:
646:
612:
559:
274:
252:
251:
249:
202:
176:
598:, 1990. (The book is out of print, but
547:A Relevant Analysis of Natural Deduction
144:and the property of being well-typed is
592:Programming in Martin-Löf's Type Theory
371:
59:. Several more recent proof tools like
585:Nordic Journal of Philosophical Logic
102:Framework = Language + Representation
7:
535:, 1988. LFCS report ECS-LFCS-88-67.
234:{\displaystyle \Lambda x\in J.K(x)}
745:, but mostly dead links from 1997)
713:
678:Representing Logics in Type Theory
651:
632:. Studia Logica 54: 199-230, 1995.
617:
607:A Note on the Proof Theory of the
276:
204:
51:. The first logical framework was
25:
689:Lecture Notes in Computer Science
384:Categorical Logic and Type Theory
73:dependently typed lambda calculus
703:A Unification Algorithm for the
669:Didier Galmiche and David Pym.
529:An Equational Formulation of LF
512:A Framework For Defining Logics
123:propositions as types principle
300:
294:
261:{\displaystyle {\mathcal {L}}}
228:
222:
155:A logic is represented in the
1:
774:Dependently typed programming
552:Samin Ishtiaq and David Pym.
545:Samin Ishtiaq and David Pym.
89:An appropriate meta-language;
719:{\displaystyle \lambda \Pi }
657:{\displaystyle \lambda \Pi }
623:{\displaystyle \lambda \Pi }
479:Proof and system-reliability
476:, Ralf Steinbrüggen (ed.).
407:Dov M. Gabbay, ed. (1994).
136:, all well-typed terms are
117:, the meta-language is the
790:
334:a logic programming engine
328:Carnegie Mellon University
759:Logic in computer science
602:has been made available.)
410:What is a logical system?
386:. Elsevier. p. 598.
190:{\displaystyle J\vdash K}
49:automated theorem proving
567:{\displaystyle \lambda }
444:. Springer. p. 48.
596:Oxford University Press
533:University of Edinburgh
96:This is summarized by:
741:(a list maintained by
720:
658:
624:
568:
313:
262:
235:
191:
79:'s system of arities.
18:LF (logical framework)
721:
659:
625:
587:", 1(1): 11-60, 1996.
569:
474:Helmut Schwichtenberg
355:Grammatical Framework
314:
263:
236:
192:
707:
645:
641:Proof-search in the
611:
558:
531:. Technical Report,
506:, Furio Honsell and
382:Bart Jacobs (2001).
273:
248:
201:
175:
157:LF logical framework
138:strongly normalizing
115:LF logical framework
113:In the case of the
39:in such a way that
716:
676:Philippa Gardner.
654:
620:
564:
360:Turnstile (symbol)
309:
258:
231:
187:
163:'s development of
579:Per Martin-Löf. "
496:978-1-4020-0608-1
451:978-3-642-03152-6
424:978-0-19-853859-2
393:978-0-444-50853-9
330:. Twelf includes
197:and the general,
45:type inhabitation
33:logical framework
16:(Redirected from
781:
769:Proof assistants
725:
723:
722:
717:
691:, 139-145, 1993.
663:
661:
660:
655:
629:
627:
626:
621:
573:
571:
570:
565:
500:
484:
456:
455:
435:
429:
428:
404:
398:
397:
379:
318:
316:
315:
310:
267:
265:
264:
259:
257:
256:
240:
238:
237:
232:
196:
194:
193:
188:
152:is undecidable.
21:
789:
788:
784:
783:
782:
780:
779:
778:
749:
748:
735:
705:
704:
643:
642:
609:
608:
556:
555:
527:Robert Harper.
497:
482:
468:
465:
463:Further reading
460:
459:
452:
437:
436:
432:
425:
417:. p. 382.
415:Clarendon Press
406:
405:
401:
394:
381:
380:
373:
368:
351:
271:
270:
246:
245:
199:
198:
173:
172:
111:
69:
23:
22:
15:
12:
11:
5:
787:
785:
777:
776:
771:
766:
761:
751:
750:
747:
746:
743:Frank Pfenning
734:
733:External links
731:
730:
729:
715:
712:
699:
692:
683:Gilles Dowek.
681:
674:
667:
653:
650:
637:Lincoln Wallen
635:David Pym and
633:
619:
616:
603:
600:a free version
588:
577:
563:
550:
543:
536:
525:
515:
508:Gordon Plotkin
501:
495:
470:Frank Pfenning
464:
461:
458:
457:
450:
430:
423:
399:
392:
370:
369:
367:
364:
363:
362:
357:
350:
347:
346:
345:
344:theorem prover
338:
335:
308:
305:
302:
299:
296:
293:
290:
287:
284:
281:
278:
255:
243:logical system
230:
227:
224:
221:
218:
215:
212:
209:
206:
186:
183:
180:
161:Per Martin-Löf
150:type inference
110:
107:
106:
105:
94:
93:
90:
87:
77:Per Martin-Löf
68:
65:
24:
14:
13:
10:
9:
6:
4:
3:
2:
786:
775:
772:
770:
767:
765:
762:
760:
757:
756:
754:
744:
740:
737:
736:
732:
727:
710:
700:
697:
693:
690:
686:
682:
679:
675:
672:
668:
665:
648:
638:
634:
631:
614:
604:
601:
597:
593:
589:
586:
582:
578:
575:
561:
551:
548:
544:
541:
537:
534:
530:
526:
523:
519:
516:
513:
509:
505:
504:Robert Harper
502:
498:
492:
488:
481:
480:
475:
471:
467:
466:
462:
453:
447:
443:
442:
434:
431:
426:
420:
416:
412:
411:
403:
400:
395:
389:
385:
378:
376:
372:
365:
361:
358:
356:
353:
352:
348:
343:
340:an inductive
339:
336:
333:
332:
331:
329:
325:
320:
306:
303:
297:
291:
288:
285:
282:
279:
244:
225:
219:
216:
213:
210:
207:
184:
181:
178:
170:
167:'s notion of
166:
162:
158:
153:
151:
147:
143:
142:Church-Rosser
139:
135:
131:
130:minimal logic
128:
124:
120:
116:
108:
103:
99:
98:
97:
91:
88:
85:
84:
83:
80:
78:
74:
66:
64:
62:
58:
54:
50:
46:
42:
38:
34:
30:
19:
702:
695:
688:
684:
677:
670:
640:
606:
591:
553:
546:
539:
528:
521:
511:
478:
440:
433:
409:
402:
383:
342:meta-logical
321:
156:
154:
114:
112:
101:
95:
81:
70:
56:
32:
26:
764:Type theory
701:David Pym.
694:David Pym.
605:David Pym.
518:Arnon Avron
148:. However,
134:predicative
127:first-order
119:λΠ-calculus
41:provability
37:type theory
753:Categories
726:-calculus.
366:References
326:system at
714:Π
711:λ
664:-calculus
652:Π
649:λ
630:-calculus
618:Π
615:λ
574:-calculus
562:λ
304:⊢
283:∈
277:Λ
211:∈
205:Λ
182:⊢
169:judgement
146:decidable
487:Springer
349:See also
67:Overview
61:Isabelle
53:Automath
493:
448:
421:
390:
483:(PDF)
324:Twelf
29:logic
583:." "
491:ISBN
446:ISBN
419:ISBN
388:ISBN
165:Kant
140:and
31:, a
125:to
27:In
755::
639:.
594:.
510:.
489:.
485:.
413:.
374:^
319:.
109:LF
104:."
57:LF
499:.
454:.
427:.
396:.
307:K
301:)
298:x
295:(
292:J
289:.
286:C
280:x
254:L
229:)
226:x
223:(
220:K
217:.
214:J
208:x
185:K
179:J
100:"
20:)
Text is available under the Creative Commons Attribution-ShareAlike License. Additional terms may apply.