An official website of the United States government
In dependently-typed functional programming languages that allow general recursion, programs used as proofs must be evaluated to retain type soundness. As a result, programmers must make a trade-off between performance and safety. To address this problem, we propose System DE, an explicitly-typed, moded core calculus that supports termination tracking and equality reflection. Programmers can write inductive proofs about potentially diverging programs in a logical sublanguage and reflect those proofs to the type checker, while knowing that such proofs will be erased by the compiler before execution. A key feature of System DE is its use of modes for both termination and relevance tracking, which not only simplifies the design but also leaves it open for future extension. System DE is suitable for use in the Glasgow Haskell Compiler, but could serve as the basis for any general purpose dependently-typed language.
more »
« less
This content will become publicly available on November 1, 2026
The ‘design features’ of language revisited
Language is often regarded as a de ning trait of our species, but what are its core properties? In 1960, Hockett published ‘The origin of speech’ enumerating 13 de- sign features presumed to be common to all languages, and which, taken to- gether, separate language from other communication systems. Here. we review which features still hold true in light of new evidence from cognitive science, lin- guistics, animal cognition, and anthropology, and demonstrate how a revised un- derstanding of language highlights three core aspects: that language is inherently multimodal and semiotically diverse; that it functions as a tool for se- mantic, pragmatic, and social inference, as well as facilitating categorization; and that the processes of interaction and transmission give rise to central design features of language.
more »
« less
- Award ID(s):
- 2020969
- PAR ID:
- 10657857
- Publisher / Repository:
- Trends in Cognitive Sciences
- Date Published:
- Journal Name:
- Trends in Cognitive Sciences
- ISSN:
- 1364-6613
- Format(s):
- Medium: X
- Sponsoring Org:
- National Science Foundation
More Like this
-
-
It is not uncommon to design a programming language as a core language with additional features that define some semantic analyses, but delegate others to their translation to the core. Many analyses require contextual information, such as a typing environment. When this is the same for a term under a new feature and under that feature’s core translation, then the term (and computations over it) can be shared, with context provided by the translation. This avoids redundant, and sometimes exponential computations. This paper brings sharing of terms and specification of context to forwarding, a language extensibility mechanism in attribute grammars. Here context is defined by equations for inherited attributes that provide (the same) values to shared trees. Applying these techniques to the ableC extensible C compiler replaced around 80% of the cases in which tree sharing was achieved by a crude mechanism that prevented sharing context specifications and limited language extensibility. It also replaced all cases in which this mechanism was used to avoid exponential computations and allowed the removal of many, now unneeded, inherited attribute equations.more » « less
-
This work proposes a novel framework for automatically scor- ing children’s oral narrative language abilities. We use audio recordings from 3rd-8th graders of the Atlanta, Georgia area as they take a portion of the Test of Narrative Language. We de- sign a system which extracts linguistic features and fine-tuned BERT-based self-supervised learning representation from state- of-the-art ASR transcripts. We predict manual test scores from the extracted features. This framework significantly outper- forms a deterministic method based on the assessment’s scoring rubric. Last, we evaluate the system performance across stu- dent’s reading level, dialect, and diagnosed learning/language disabilities to establish fairness across diverse demographics of students. Using this system, we achieve approximately 98% classification accuracy of student scores. We are also able to identify key areas of improvement for this type of system across demographic areas and reading ability.more » « less
-
P4 is a domain-specific language for programming and specifying packet-processing systems. It is based on an elegant design with high-level abstractions like parsers and match-action pipelines that can be compiled to efficient implementations in software or hardware. Unfortunately, like many industrial languages, P4 has developed without a formal foundation. The P4 Language Specification is a 160-page document with a mixture of informal prose, graphical diagrams, and pseudocode, leaving many aspects of the language semantics up to individual compilation targets. The P4 reference implementation is a complex system, running to over 40KLoC of C++ code, with support for only a few targets. Clearly neither of these artifacts is suitable for formal reasoning about P4 in general. This paper presents a new framework, called Petr4, that puts P4 on a solid foundation. Petr4 consists of a clean-slate definitional interpreter and a core calculus that models a fragment of P4. Petr4 is not tied to any particular target: the interpreter is parameterized over an interface that collects features delegated to targets in one place, while the core calculus overapproximates target-specific behaviors using non-determinism. We have validated the interpreter against a suite of over 750 tests from the P4 reference implementation, exercising our target interface with tests for different targets. We validated the core calculus with a proof of type-preserving termination. While developing Petr4, we reported dozens of bugs in the language specification and the reference implementation, many of which have been fixed.more » « less
-
Abstract The language contact between Basque and Spanish in the Basque Autonomous Community (BAC) gives rise to the production of specific linguistic features such as non-standard gender agreement (N-SGA). N-SGA in BAC Spanish has been traditionally attributed to elder Basque native speakers without much access to education, but this affirmation is not based on any empirical study. In addition, although several scholars have explored N-SGA in other language contact situations, there is no agreement on the linguistic factors that favor this production. Taking this knowledge gap as the point of departure, the present study explores 73 individual sociolinguistic interviews by a diverse population from the BAC in order to delimit (i) the community that produces N-SGA and (ii) the linguistic factors that condition it. Results follow Basterretxea Santiso’s (2022, “A triangulation study on gender agreement in Spanish by native Basque speakers.”Revista Española de Lingüística (RSEL)52(1): 7–37) suggestion that N-SGA in BAC Spanish is present across generations: it is a well-established feature present in BAC Spanish as a result of language contact. Results also support the existence of a local gender agreement system that depends on the gender of the controller, inflectional form, number, distance, and whether the target is a clitic or adjective.more » « less
